diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/environ.ml | 9 | ||||
| -rw-r--r-- | kernel/term.ml | 66 | ||||
| -rw-r--r-- | kernel/term.mli | 6 |
3 files changed, 76 insertions, 5 deletions
diff --git a/kernel/environ.ml b/kernel/environ.ml index fdfc540d26..4471d5b873 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -103,10 +103,10 @@ let add_abstraction sp ab env = env_abstractions = new_abs; env_locals = new_locals } in { env with env_globals = new_globals } - -let new_meta = - let meta_ctr = ref 0 in - fun () -> (incr meta_ctr; !meta_ctr) + +let meta_ctr=ref 0;; + +let new_meta ()=incr meta_ctr;!meta_ctr;; (* Access functions. *) @@ -310,4 +310,3 @@ type unsafe_judgment = { let cast_of_judgment = function | { uj_val = DOP2 (Cast,_,_) as c } -> c | { uj_val = c; uj_type = ty } -> mkCast c ty - diff --git a/kernel/term.ml b/kernel/term.ml index a83a8c6f23..16d63fcbfc 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -1307,6 +1307,21 @@ let rec occur_meta = function | DOP0(Meta(_)) -> true | _ -> false +(*Returns the maximum of metas. Returns -1 if there is no meta*) +(*let rec max_occur_meta=function + DOP2(Prod,t,DLAM(_,c)) -> + max (max_occur_meta t) (max_occur_meta c) + |DOP2(Lambda,t,DLAM(_,c)) -> + max (max_occur_meta t) (max_occur_meta c) + |DOPN(_,cl) -> + (try + List.hd (Sort.list (>) (List.map max_occur_meta (Array.to_list cl))) + with + Failure "hd" -> -1) + |DOP2(Cast,c,t) -> max (max_occur_meta c) (max_occur_meta t) + |DOP0(Meta n) -> n + |_ -> -1;;*) + let rel_vect = (Generic.rel_vect : int -> int -> constr array) let occur_existential = @@ -1584,3 +1599,54 @@ let sub_term_with_unif cref ceq= None else Some ((subst_with_lmeta l ceq),nb) + +let constr_display csr= + let rec term_display=function + DOP0(a) -> "DOP0("^(oper_display a)^")" + |DOP1(a,b) -> "DOP1("^(oper_display a)^","^(term_display b)^")" + |DOP2(a,b,c) -> + "DOP2("^(oper_display a)^","^(term_display b)^","^(term_display c)^")" + |DOPN(a,b) -> + "DOPN("^(oper_display a)^",[|"^(Array.fold_right (fun x i -> + (term_display x)^(if not(i="") then (";"^i) else "")) b "")^"|])" + |DOPL(a,b) -> + "DOPL("^(oper_display a)^",[|"^(List.fold_right (fun x i -> + (term_display x)^(if not(i="") then (";"^i) else "")) b "")^"|]" + |DLAM(a,b) -> "DLAM("^(name_display a)^","^(term_display b)^")" + |DLAMV(a,b) -> + "DLAMV("^(name_display a)^",[|"^(Array.fold_right (fun x i -> + (term_display x)^(if not(i="") then (";"^i) else "")) b "")^"|]" + |VAR(a) -> "VAR "^(string_of_id a) + |Rel(a) -> "Rel "^(string_of_int a) + and oper_display=function + Meta(a) -> "?"^(string_of_int a) +(* |XTRA(a,_) -> "XTRA("^a^",[ast])"*) + |Sort(a) -> "Sort("^(sort_display a)^")" +(* |Implicit -> "Implicit"*) + |Cast -> "Cast" + |Prod -> "Prod" + |Lambda -> "Lambda" + |AppL -> "AppL" + |Const(sp) -> "Const("^(string_of_path sp)^")" + |Abst(sp) -> "Abst("^(string_of_path sp)^")" + |MutInd(sp,i) -> "MutInd("^(string_of_path sp)^","^(string_of_int i)^")" + |MutConstruct((sp,i),j) -> + "MutConstruct(("^(string_of_path sp)^","^(string_of_int i)^"),"^ + (string_of_int j)^")" +(* |MutCase(ci) -> "MutCase("^(ci_display ci)^")"*) + |Fix(t,i) -> + "Fix([|"^(Array.fold_right (fun x i -> (string_of_int x)^(if not(i="") + then (";"^i) else "")) t "")^"|],"^(string_of_int i)^")" + |CoFix(i) -> "CoFix "^(string_of_int i) + and sort_display=function + Prop(Pos) -> "Prop(Pos)" + |Prop(Null) -> "Prop(Null)" + |Type(_) -> "Type" +(* and ci_display=function + Some(sp,i) -> "Some("^(string_of_path sp)^","^(string_of_int i)^")" + |None -> "None"*) + and name_display=function + Name(id) -> "Name("^(string_of_id id)^")" + |Anonymous -> "Anonymous" + in + mSG [<'sTR (term_display csr);'fNL>];; diff --git a/kernel/term.mli b/kernel/term.mli index dc9684b923..145546b55c 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -514,6 +514,10 @@ val sort_hdchar : sorts -> string (*s Occur check functions. *) val occur_meta : constr -> bool + +(*Returns the maximum of metas. Returns -1 if there is no meta*) +(*val max_occur_meta:constr->int;;*) + val occur_existential : constr -> bool val rel_vect : int -> int -> constr array @@ -557,3 +561,5 @@ val hcons_constr: (typed_type -> typed_type) val hcons1_constr : constr -> constr + +val constr_display: constr -> unit;; |