diff options
Diffstat (limited to 'program/reducer.prim')
| -rw-r--r-- | program/reducer.prim | 50 |
1 files changed, 25 insertions, 25 deletions
diff --git a/program/reducer.prim b/program/reducer.prim index 0a0517e..3abbc97 100644 --- a/program/reducer.prim +++ b/program/reducer.prim @@ -1,16 +1,16 @@ -let Bool = [T: <>, F: <>] in +let Bool = [T: <>; F: <>] in let or (x : Bool) (y : Bool) : Bool = case x of {T u => T <>; F u => y} in let SysT = (\T => [ Var: Nat - , Zero: <> - , Suc: T - , Primrec: <Zero: T, Suc: T, Target: T> - , Abs: T - , App: <Fun: T, Arg: T> + ; Zero: <> + ; Suc: T + ; Primrec: <Zero: T; Suc: T; Target: T> + ; Abs: T + ; App: <Fun: T; Arg: T> ]) in -let Stepped = <Term: SysT, Smaller: Bool> in +let Stepped = <Term: SysT; Smaller: Bool> in let lift (f : Nat -> Nat) (n : Nat) : Nat = case !n of {Z u => 0; S k => suc (f k)} in @@ -20,9 +20,9 @@ let rename (t : SysT) : (Nat -> Nat) -> SysT = ; Zero u => \f => ~(Zero <>) ; Suc r => \f => ~(Suc (r f)) ; Primrec p => \f => - ~(Primrec <Zero: p.Zero f, Suc: p.Suc (lift f), Target: p.Target f>) + ~(Primrec <Zero: p.Zero f; Suc: p.Suc (lift f); Target: p.Target f>) ; Abs r => \f => ~(Abs (r f)) - ; App p => \f => ~(App <Fun: p.Fun f, Arg: p.Arg f>) + ; App p => \f => ~(App <Fun: p.Fun f; Arg: p.Arg f>) } in let index (xs : List SysT) : Nat -> SysT = @@ -40,35 +40,35 @@ let sub (t : SysT) : List SysT -> SysT = ; Primrec p => \env => ~(Primrec < Zero: p.Zero env - , Suc: p.Suc (cons ~(Var 0) (shift env)) - , Target: p.Target env + ; Suc: p.Suc (cons ~(Var 0) (shift env)) + ; Target: p.Target env >) ; Abs f => \env => ~(Abs (f (cons ~(Var 0) (shift env)))) - ; App p => \env => ~(App <Fun: p.Fun env, Arg: p.Arg env>) + ; App p => \env => ~(App <Fun: p.Fun env; Arg: p.Arg env>) } in let app (fun : SysT) (arg : SysT) (smaller : Bool) : Stepped = let default : Stepped = - <Term: ~(App <Fun: fun, Arg: arg>), Smaller: smaller> + <Term: ~(App <Fun: fun; Arg: arg>); Smaller: smaller> in case !fun of { Var n => default ; Zero u => default ; Suc t => default ; Primrec p => default - ; Abs t => <Term: sub t [arg], Smaller: T <>> + ; Abs t => <Term: sub t [arg]; Smaller: T <>> ; App t => default } in let rec (z : SysT) (s : SysT) (target : SysT) (smaller : Bool) : Stepped = let default : Stepped = - <Term: ~(Primrec <Zero: z, Suc: s, Target: target>), Smaller: smaller> + <Term: ~(Primrec <Zero: z; Suc: s; Target: target>); Smaller: smaller> in case !target of { Var n => default - ; Zero u => <Term: z, Smaller: T <>> + ; Zero u => <Term: z; Smaller: T <>> ; Suc t => - <Term: sub s [~(Primrec <Zero: z, Suc: s, Target: t>)], Smaller: T <>> + <Term: sub s [~(Primrec <Zero: z; Suc: s; Target: t>)]; Smaller: T <>> ; Primrec p => default ; Abs t => default ; App t => default @@ -76,9 +76,9 @@ let rec (z : SysT) (s : SysT) (target : SysT) (smaller : Bool) : Stepped = in let step (t : SysT) : Stepped = foldcase t by - { Var n => <Term: ~(Var n), Smaller: F <>> - ; Zero u => <Term: ~(Zero <>), Smaller: F <>> - ; Suc t => <Term: ~(Suc t.Term), Smaller: t.Smaller> + { Var n => <Term: ~(Var n); Smaller: F <>> + ; Zero u => <Term: ~(Zero <>); Smaller: F <>> + ; Suc t => <Term: ~(Suc t.Term); Smaller: t.Smaller> ; Primrec t => case t.Target.Smaller of { F u => @@ -91,22 +91,22 @@ let step (t : SysT) : Stepped = < Term: ~(Primrec (map - (\X => <Zero: X, Suc: X, Target: X>) + (\X => <Zero: X; Suc: X; Target: X>) Stepped SysT (\p => p.Term) t)) - , Smaller: T <> + ; Smaller: T <> > } - ; Abs t => <Term: ~(Abs t.Term), Smaller: t.Smaller> + ; Abs t => <Term: ~(Abs t.Term); Smaller: t.Smaller> ; App t => case t.Arg.Smaller of { F u => app t.Fun.Term t.Arg.Term t.Fun.Smaller ; T u => < Term: - ~(App (map (\X => <Fun: X, Arg: X>) Stepped SysT (\p => p.Term) t)) - , Smaller: T <> + ~(App (map (\X => <Fun: X; Arg: X>) Stepped SysT (\p => p.Term) t)) + ; Smaller: T <> > } } |