cicCooking.ml* forgot in the previous commit

[helm.git] / helm / ocaml / cic_proof_checking / cicPp.ml

diff --git a/helm/ocaml/cic_proof_checking/cicPp.ml b/helm/ocaml/cic_proof_checking/cicPp.ml
index 07e306b0be83e167708dd4a05266205e166bbeb1..05c964370b7b711941fc1a9a0930851058f60a37 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicPp.ml
+++ b/helm/ocaml/cic_proof_checking/cicPp.ml
@@ -44,7 +44,7 @@ exception NotEnoughElements;;
 let string_of_name =
  function
     Cic.Name s     -> s
-  | Cic.Anonimous  -> "_"
+  | Cic.Anonymous  -> "_"
 ;;
 
 (* get_nth l n   returns the nth element of the list l if it exists or *)
@@ -68,12 +68,14 @@ let rec pp t l =
         try
          (match get_nth l n with
              Some (C.Name s) -> s
-           | _        -> raise CicPpInternalError
+           | Some C.Anonymous -> "__" ^ string_of_int n
+           | _ -> raise CicPpInternalError
          )
         with
          NotEnoughElements -> string_of_int (List.length l - n)
        end
-    | C.Var uri -> UriManager.name_of_uri uri
+    | C.Var (uri,exp_named_subst) ->
+       UriManager.string_of_uri (*UriManager.name_of_uri*) uri ^ pp_exp_named_subst exp_named_subst l
     | C.Meta (n,l1) ->
        "?" ^ (string_of_int n) ^ "[" ^ 
         String.concat " ; "
@@ -89,7 +91,7 @@ let rec pp t l =
     | C.Prod (b,s,t) ->
        (match b with
           C.Name n -> "(" ^ n ^ ":" ^ pp s l ^ ")" ^ pp t ((Some b)::l)
-        | C.Anonimous -> "(" ^ pp s l ^ "->" ^ pp t ((Some b)::l) ^ ")"
+        | C.Anonymous -> "(" ^ pp s l ^ "->" ^ pp t ((Some b)::l) ^ ")"
        )
     | C.Cast (v,t) -> pp v l
     | C.Lambda (b,s,t) ->
@@ -102,29 +104,29 @@ let rec pp t l =
         (fun x i -> pp x l ^ (match i with "" -> "" | _ -> " ") ^ i)
         li ""
        ) ^ ")"
-    | C.Const (uri,_) -> UriManager.name_of_uri uri
-    | C.Abst uri -> UriManager.name_of_uri uri
-    | C.MutInd (uri,_,n) ->
+    | C.Const (uri,exp_named_subst) ->
+       UriManager.name_of_uri uri ^ pp_exp_named_subst exp_named_subst l
+    | C.MutInd (uri,n,exp_named_subst) ->
        (match CicEnvironment.get_obj uri with
            C.InductiveDefinition (dl,_,_) ->
             let (name,_,_,_) = get_nth dl (n+1) in
-             name
+             name ^ pp_exp_named_subst exp_named_subst l
          | _ -> raise CicPpInternalError
        )
-    | C.MutConstruct (uri,_,n1,n2) ->
+    | C.MutConstruct (uri,n1,n2,exp_named_subst) ->
        (match CicEnvironment.get_obj uri with
            C.InductiveDefinition (dl,_,_) ->
             let (_,_,_,cons) = get_nth dl (n1+1) in
-             let (id,_,_) = get_nth cons n2 in
-              id
+             let (id,_) = get_nth cons n2 in
+              id ^ pp_exp_named_subst exp_named_subst l
          | _ -> raise CicPpInternalError
        )
-    | C.MutCase (uri,_,n1,ty,te,patterns) ->
+    | C.MutCase (uri,n1,ty,te,patterns) ->
        let connames =
         (match CicEnvironment.get_obj uri with
             C.InductiveDefinition (dl,_,_) ->
              let (_,_,_,cons) = get_nth dl (n1+1) in
-              List.map (fun (id,_,_) -> id) cons
+              List.map (fun (id,_) -> id) cons
           | _ -> raise CicPpInternalError
         )
        in
@@ -156,6 +158,14 @@ let rec pp t l =
             pp bo (names@l) ^ i)
           funs "" ^
          "}\n"
+and pp_exp_named_subst exp_named_subst l =
+ if exp_named_subst = [] then "" else
+  "{" ^
+   String.concat " ; " (
+    List.map
+     (function (uri,t) -> UriManager.name_of_uri uri ^ ":=" ^ pp t l)
+     exp_named_subst
+   ) ^ "}"
 ;;
 
 let ppterm t =
@@ -173,7 +183,7 @@ let ppinductiveType (typename, inductive, arity, cons) names =
   (*CSC: bug found: was pp arity names ^ " =\n   " ^*)
   pp arity [] ^ " =\n   " ^
   List.fold_right
-   (fun (id,ty,_) i -> id ^ " : " ^ pp ty names ^ 
+   (fun (id,ty) i -> id ^ " : " ^ pp ty names ^ 
     (if i = "" then "\n" else "\n | ") ^ i)
    cons ""
 ;;
@@ -184,32 +194,24 @@ let ppobj obj =
  let module C = Cic in
  let module U = UriManager in
   match obj with
-    C.Definition (id, t1, t2, params) ->
-      "Definition of " ^ id ^
-      "(" ^
-      List.fold_right
-       (fun (_,x) i ->
-         List.fold_right
-          (fun x i ->
-            U.string_of_uri x ^ match i with "" -> "" | i' -> " " ^ i'
-          ) x "" ^ match i with "" -> "" | i' -> " " ^ i'
-       ) params "" ^ ")" ^
-      ":\n" ^ pp t1 [] ^ " : " ^ pp t2 []
-   | C.Axiom (id, ty, params) ->
-      "Axiom " ^ id ^ "(" ^
-      List.fold_right
-       (fun (_,x) i ->
-         List.fold_right
-          (fun x i ->
-            U.string_of_uri x ^ match i with "" -> "" | i' -> " " ^ i'
-          ) x "" ^ match i with "" -> "" | i' -> " " ^ i'
-       ) params "" ^
-      "):\n" ^ pp ty []
-   | C.Variable (name, bo, ty) ->
-      "Variable " ^ name ^ ":\n" ^ pp ty [] ^ "\n" ^
-      (match bo with None -> "" | Some bo -> ":= " ^ pp bo [])
-   | C.CurrentProof (name, conjectures, value, ty) ->
-      "Current Proof:\n" ^
+    C.Constant (name, Some t1, t2, params) ->
+      "Definition of " ^ name ^
+       "(" ^ String.concat ";" (List.map UriManager.string_of_uri params) ^
+       ")" ^ ":\n" ^ pp t1 [] ^ " : " ^ pp t2 []
+   | C.Constant (name, None, ty, params) ->
+      "Axiom " ^ name ^
+       "(" ^ String.concat ";" (List.map UriManager.string_of_uri params) ^
+       "):\n" ^ pp ty []
+   | C.Variable (name, bo, ty, params) ->
+      "Variable " ^ name ^
+       "(" ^ String.concat ";" (List.map UriManager.string_of_uri params) ^
+       ")" ^ ":\n" ^
+       pp ty [] ^ "\n" ^
+       (match bo with None -> "" | Some bo -> ":= " ^ pp bo [])
+   | C.CurrentProof (name, conjectures, value, ty, params) ->
+      "Current Proof of " ^ name ^
+       "(" ^ String.concat ";" (List.map UriManager.string_of_uri params) ^
+       ")" ^ ":\n" ^
       let separate s = if s = "" then "" else s ^ " ; " in
        List.fold_right
         (fun (n, context, t) i -> 
@@ -235,14 +237,8 @@ let ppobj obj =
         "\n" ^ pp value [] ^ " : " ^ pp ty [] 
    | C.InductiveDefinition (l, params, nparams) ->
       "Parameters = " ^
-      List.fold_right
-       (fun (_,x) i ->
-         List.fold_right
-          (fun x i ->
-            U.string_of_uri x ^ match i with "" -> "" | i' -> " " ^ i'
-          ) x "" ^ match i with "" -> "" | i' -> " " ^ i'
-       ) params "" ^ "\n" ^
-      "NParams = " ^ string_of_int nparams ^ "\n" ^
-      let names = List.rev (List.map (fun (n,_,_,_) -> Some (C.Name n)) l) in
-       List.fold_right (fun x i -> ppinductiveType x names ^ i) l ""
+       String.concat ";" (List.map UriManager.string_of_uri params) ^ "\n" ^
+       "NParams = " ^ string_of_int nparams ^ "\n" ^
+       let names = List.rev (List.map (fun (n,_,_,_) -> Some (C.Name n)) l) in
+        List.fold_right (fun x i -> ppinductiveType x names ^ i) l ""
 ;;