Ajout du langage de tactiques

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@401 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 66 insertions, 0 deletions

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>];;