(* stdlib.ml: type environment and symboltable for predefined variables *) (* $Id: stdlib.ml,v 1.10 2000/07/20 01:45:54 alamstei Exp $ *) open Lambda open Types open Pseudo exception Not_reduced;; let a = Usertvar "a" let b = Usertvar "b" let rec reduce_opt_step term = match term with (* arithmetic basic functions *) App(App(Var(Uservar "plus"),Intlit m), Intlit n) -> Intlit(m+n) | App(App(Var(Uservar "minus"),Intlit m), Intlit n) -> Intlit(m-n) | App(App(Var(Uservar "mult"),Intlit m), Intlit n) -> Intlit(m*n) | App(App(Var(Uservar "divide"),Intlit m), Intlit n) -> Intlit(m/n) | App(App(Var(Uservar "mod"),Intlit m), Intlit n) -> Intlit(m mod n) | App(App(Var(Uservar "greater"),Intlit m), Intlit n) -> Boollit(m>n) | App(App(Var(Uservar "geq"),Intlit m), Intlit n) -> Boollit(m>=n) | App(App(Var(Uservar "less"),Intlit m), Intlit n) -> Boollit(m Boollit(m<=n) | App(App(Var(Uservar "equal"),Intlit m), Intlit n) -> Boollit(m=n) | App(App(Var(Uservar "neq"),Intlit m), Intlit n) -> Boollit(m<>n) (* logical and misc. operations *) | App(App(Var(Uservar "and"),Boollit m), Boollit n) -> Boollit(m&&n) | App(App(Var(Uservar "or"),Boollit m), Boollit n) -> Boollit(m||n) | App(Var(Uservar "not"),Boollit m) -> Boollit(not(m)) | App(App(App(Var(Uservar "if"),Boollit m),n),p) -> if m then n else p | _ -> raise Not_reduced let reduce_cbn term reduce normalform = let must_reduce m errormsg = try reduce m with e when e=normalform -> raise (Exn.Runtimeerror(errormsg,term)) in match term with | App(App(Var(Uservar "plus"), Intlit m), Intlit n) -> Intlit(m+n) | App(App(Var(Uservar "plus"), Intlit m), n) -> let n' = must_reduce n "illegal argument for plus" in App(App(Var(Uservar "plus"), Intlit m), n') | App(App(Var(Uservar "plus"), m), n) -> let m' = must_reduce m "illegal argument for plus" in App(App(Var(Uservar "plus"), m'), n) | App(Var(Uservar "plus"), m) -> raise normalform | App(App(Var(Uservar "minus"), Intlit m), Intlit n) -> Intlit(m-n) | App(App(Var(Uservar "minus"), Intlit m), n) -> let n' = must_reduce n "illegal argument for minus" in App(App(Var(Uservar "minus"), Intlit m), n') | App(App(Var(Uservar "minus"), m), n) -> let m' = must_reduce m "illegal argument for minus" in App(App(Var(Uservar "minus"), m'), n) | App(Var(Uservar "minus"), m) -> raise normalform | App(App(Var(Uservar "mult"), Intlit m), Intlit n) -> Intlit(m*n) | App(App(Var(Uservar "mult"), Intlit m), n) -> let n' = must_reduce n "illegal argument for mult" in App(App(Var(Uservar "mult"), Intlit m), n') | App(App(Var(Uservar "mult"), m), n) -> let m' = must_reduce m "illegal argument for mult" in App(App(Var(Uservar "mult"), m'), n) | App(Var(Uservar "mult"), m) -> raise normalform | App(App(Var(Uservar "divide"), Intlit m), Intlit n) -> Intlit(m/n) | App(App(Var(Uservar "divide"), Intlit m), n) -> let n' = must_reduce n "illegal argument for divide" in App(App(Var(Uservar "divide"), Intlit m), n') | App(App(Var(Uservar "divide"), m), n) -> let m' = must_reduce m "illegal argument for divide" in App(App(Var(Uservar "divide"), m'), n) | App(Var(Uservar "divide"), m) -> raise normalform | App(App(Var(Uservar "mod"), Intlit m), Intlit n) -> Intlit(m mod n) | App(App(Var(Uservar "mod"), Intlit m), n) -> let n' = must_reduce n "illegal argument for mod" in App(App(Var(Uservar "mod"), Intlit m), n') | App(App(Var(Uservar "mod"), m), n) -> let m' = must_reduce m "illegal argument for mod" in App(App(Var(Uservar "mod"), m'), n) | App(Var(Uservar "mod"), m) -> raise normalform | App(App(Var(Uservar "greater"), Intlit m), Intlit n) -> Boollit(m>n) | App(App(Var(Uservar "greater"), Intlit m), n) -> let n' = must_reduce n "illegal argument for greater" in App(App(Var(Uservar "greater"), Intlit m), n') | App(App(Var(Uservar "greater"), m), n) -> let m' = must_reduce m "illegal argument for greater" in App(App(Var(Uservar "greater"), m'), n) | App(Var(Uservar "greater"), m) -> raise normalform | App(App(Var(Uservar "geq"), Intlit m), Intlit n) -> Boollit(m>=n) | App(App(Var(Uservar "geq"), Intlit m), n) -> let n' = must_reduce n "illegal argument for geq" in App(App(Var(Uservar "geq"), Intlit m), n') | App(App(Var(Uservar "geq"), m), n) -> let m' = must_reduce m "illegal argument for geq" in App(App(Var(Uservar "geq"), m'), n) | App(Var(Uservar "geq"), m) -> raise normalform | App(App(Var(Uservar "less"), Intlit m), Intlit n) -> Boollit(m let n' = must_reduce n "illegal argument for less" in App(App(Var(Uservar "less"), Intlit m), n') | App(App(Var(Uservar "less"), m), n) -> let m' = must_reduce m "illegal argument for less" in App(App(Var(Uservar "less"), m'), n) | App(Var(Uservar "less"), m) -> raise normalform | App(App(Var(Uservar "leq"), Intlit m), Intlit n) -> Boollit(m<=n) | App(App(Var(Uservar "leq"), Intlit m), n) -> let n' = must_reduce n "illegal argument for leq" in App(App(Var(Uservar "leq"), Intlit m), n') | App(App(Var(Uservar "leq"), m), n) -> let m' = must_reduce m "illegal argument for leq" in App(App(Var(Uservar "leq"), m'), n) | App(Var(Uservar "leq"), m) -> raise normalform | App(App(Var(Uservar "equal"), Intlit m), Intlit n) -> Boollit(m=n) | App(App(Var(Uservar "equal"), Intlit m), n) -> let n' = must_reduce n "illegal argument for equal" in App(App(Var(Uservar "equal"), Intlit m), n') | App(App(Var(Uservar "equal"), m), n) -> let m' = must_reduce m "illegal argument for equal" in App(App(Var(Uservar "equal"), m'), n) | App(Var(Uservar "equal"), m) -> raise normalform | App(App(Var(Uservar "neq"), Intlit m), Intlit n) -> Boollit(m<>n) | App(App(Var(Uservar "neq"), Intlit m), n) -> let n' = must_reduce n "illegal argument for neq" in App(App(Var(Uservar "neq"), Intlit m), n') | App(App(Var(Uservar "neq"), m), n) -> let m' = must_reduce m "illegal argument for neq" in App(App(Var(Uservar "neq"), m'), n) | App(Var(Uservar "neq"), m) -> raise normalform | App(App(Var(Uservar "and"), Boollit m), Boollit n) -> Boollit(m&&n) | App(App(Var(Uservar "and"), Boollit m), n) -> let n' = must_reduce n "illegal argument for and" in App(App(Var(Uservar "and"), Boollit m), n') | App(App(Var(Uservar "and"), m), n) -> let m' = must_reduce m "illegal argument for and" in App(App(Var(Uservar "and"), m'), n) | App(Var(Uservar "and"), m) -> raise normalform | App(App(Var(Uservar "or"), Boollit m), Boollit n) -> Boollit(m||n) | App(App(Var(Uservar "or"), Boollit m), n) -> let n' = must_reduce n "illegal argument for or" in App(App(Var(Uservar "or"), Boollit m), n') | App(App(Var(Uservar "or"), m), n) -> let m' = must_reduce m "illegal argument for or" in App(App(Var(Uservar "or"), m'), n) | App(Var(Uservar "or"), m) -> raise normalform | App(Var(Uservar "not"), Boollit m) -> Boollit(not m) | App(Var(Uservar "not"), m) -> let m' = must_reduce m "illegal argument for not" in App(Var(Uservar "not"), m') | App(App(App(Var(Uservar "if"), Boollit m),n),p) -> if m then n else p | App(App(App(Var(Uservar "if"), m),n),p) -> let m' = must_reduce m "illegal argument for if" in App(App(App(Var(Uservar "if"), m'),n),p) | _ -> raise Not_reduced let stdcontext = [ (* arithmetic operations *) (Uservar "plus", ([],Arrow(Int, Arrow(Int, Int)))); (Uservar "minus", ([],Arrow(Int, Arrow(Int, Int)))); (Uservar "mult", ([],Arrow(Int, Arrow(Int, Int)))); (Uservar "divide", ([],Arrow(Int, Arrow(Int, Int)))); (Uservar "mod", ([],Arrow(Int, Arrow(Int, Int)))); (Uservar "greater", ([],Arrow(Int,Arrow(Int,Bool)))); (Uservar "geq", ([],Arrow(Int,Arrow(Int,Bool)))); (Uservar "less", ([],Arrow(Int,Arrow(Int,Bool)))); (Uservar "leq", ([],Arrow(Int,Arrow(Int,Bool)))); (Uservar "equal", ([],Arrow(Int,Arrow(Int, Bool)))); (Uservar "neq", ([],Arrow(Int,Arrow(Int, Bool)))); (* logical and misc. operations *) (Uservar "and", ([],Arrow(Bool,Arrow(Bool,Bool)))); (Uservar "or", ([],Arrow(Bool,Arrow(Bool,Bool)))); (Uservar "not", ([],Arrow(Bool,Bool))); (Uservar "if", ([a],Arrow(Bool,Arrow(TVar a,Arrow(TVar a,TVar a))))); (Uservar "match#failure", ([a;b],Arrow(TVar a, TVar b))); ] let stdbindings = [ (* arithmetic operations *) (Uservar "plus", Label "plus_c"); (Uservar "minus", Label "minus_c"); (Uservar "mult", Label "mult_c"); (Uservar "divide", Label "divide_c"); (Uservar "mod", Label "mod_c"); (Uservar "equal", Label "equal_c"); (Uservar "neq", Label "neq_c"); (Uservar "greater", Label "greater_c"); (Uservar "geq", Label "geq_c"); (Uservar "less", Label "less_c"); (Uservar "leq", Label "leq_c"); (* logical and misc. operations *) (Uservar "and", Label "and_c"); (Uservar "or", Label "or_c"); (Uservar "not", Label "not_c"); (Uservar "if", Label "if_c"); (Uservar "match#failure", Label "match_failure_c"); ]