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