1structure Rsyntax :> Rsyntax = 2struct 3 4 type thm = Thm.thm; 5 type term = Term.term; 6 type hol_type = Type.hol_type; 7 8 9fun mk_type{Tyop,Args} = Type.mk_type(Tyop,Args) 10fun mk_var{Name,Ty} = Term.mk_var(Name,Ty) 11fun mk_primed_var{Name,Ty} = Term.mk_primed_var(Name,Ty) 12fun mk_const{Name,Ty} = Term.mk_const(Name,Ty) 13fun mk_comb{Rator,Rand} = Term.mk_comb(Rator,Rand) 14fun mk_abs{Bvar,Body} = Term.mk_abs(Bvar,Body) 15fun mk_eq{lhs,rhs} = boolSyntax.mk_eq(lhs,rhs) 16fun mk_imp{ant,conseq} = boolSyntax.mk_imp(ant,conseq) 17fun mk_forall{Bvar,Body} = boolSyntax.mk_forall(Bvar,Body) 18fun mk_exists{Bvar,Body} = boolSyntax.mk_exists(Bvar,Body) 19fun mk_exists1{Bvar,Body} = boolSyntax.mk_exists1(Bvar,Body) 20fun mk_select{Bvar,Body} = boolSyntax.mk_select(Bvar,Body) 21fun mk_conj{conj1,conj2} = boolSyntax.mk_conj(conj1,conj2) 22fun mk_disj{disj1,disj2} = boolSyntax.mk_disj(disj1,disj2) 23fun mk_let{func,arg} = boolSyntax.mk_let(func,arg) 24fun mk_cond{cond,larm,rarm} = boolSyntax.mk_cond(cond,larm,rarm); 25 26fun dest_type ty = let val (s,l) = Type.dest_type ty in {Tyop=s,Args=l} end 27fun dest_var M = let val (s,ty) = Term.dest_var M in {Name=s,Ty=ty} end 28fun dest_const M = let val (s,ty) = Term.dest_const M in {Name=s,Ty=ty} end 29fun dest_comb M = let val (f,x) = Term.dest_comb M in {Rator=f,Rand=x} end 30fun dest_abs M = let val (v,N) = Term.dest_abs M in {Bvar=v,Body=N} end; 31 32fun dest_eq M = let val (l,r) = boolSyntax.dest_eq M in {lhs=l,rhs=r} end; 33fun dest_imp M = let val (l,r) = boolSyntax.dest_imp M in {ant=l,conseq=r} end; 34fun dest_imp_only M = 35 let val (l,r) = boolSyntax.dest_imp_only M in {ant=l,conseq=r} end; 36fun dest_select M = 37 let val (v,N) = boolSyntax.dest_select M in {Bvar=v,Body=N} end; 38fun dest_forall M = 39 let val (v,N) = boolSyntax.dest_forall M in {Bvar=v,Body=N} end; 40fun dest_exists M = 41 let val (v,N) = boolSyntax.dest_exists M in {Bvar=v,Body=N} end; 42fun dest_exists1 M = 43 let val (v,N) = boolSyntax.dest_exists1 M in {Bvar=v,Body=N} end; 44fun dest_conj M = 45 let val (l,r) = boolSyntax.dest_conj M in {conj1=l,conj2=r} end; 46fun dest_disj M = 47 let val (l,r) = boolSyntax.dest_disj M in {disj1=l,disj2=r} end; 48fun dest_cond M = 49 let val (b,l,r) = boolSyntax.dest_cond M in {cond=b,larm=l,rarm=r} end 50fun dest_let M = let val (f,a) = boolSyntax.dest_let M in {func=f,arg=a} end; 51 52fun new_type{Name,Arity} = boolSyntax.new_type(Name,Arity); 53fun new_constant{Name,Ty} = boolSyntax.new_constant(Name,Ty); 54fun new_infix{Name,Prec,Ty} = boolSyntax.new_infix(Name,Ty,Prec); 55fun new_binder{Name,Ty} = boolSyntax.new_binder(Name,Ty); 56 57fun new_specification {name,sat_thm,consts} = let 58 open Parse 59 val cnames = map #const_name consts 60 val res = Theory.Definition.new_specification(name, cnames, sat_thm) 61 fun modify_grammar {const_name,fixity=SOME fxty} = set_fixity const_name fxty 62 | modify_grammar _ = () 63in 64 app modify_grammar consts; 65 res 66end; 67 68datatype lambda 69 = VAR of {Name:string, Ty:hol_type} 70 | CONST of {Name:string, Thy:string, Ty:hol_type} 71 | COMB of {Rator:term, Rand:term} 72 | LAMB of {Bvar:term, Body:term}; 73 74local open Feedback 75in 76fun dest_term M = 77 case Term.dest_term M of 78 Term.COMB(t1,t2) => COMB{Rator = t1, Rand = t2} 79 | Term.LAMB(v,b) => LAMB{Bvar = v, Body = b} 80 | Term.CONST r => CONST r 81 | Term.VAR (n,ty) => VAR{Name = n, Ty = ty} 82end; 83 84end (* Rsyntax *) 85