prima implementazione di demodulate, superposition_left e superposition_right

[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 49d004ee0201d765c6a9445c172d38f24294091b..d9c669ed570e318173056744488fa88b58ab4876 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicPp.ml
+++ b/helm/ocaml/cic_proof_checking/cicPp.ml
@@ -85,7 +85,8 @@ let rec pp t l =
        (match s with
            C.Prop  -> "Prop"
          | C.Set   -> "Set"
-         | C.Type _ -> "Type" (* TASSI: universe is not explicit *)
+         | C.Type _ -> "Type"
+         (*| C.Type u -> ("Type" ^ CicUniv.string_of_universe u)*)
         | C.CProp -> "CProp" 
        )
     | C.Implicit _ -> "?"
@@ -94,7 +95,7 @@ let rec pp t l =
           C.Name n -> "(" ^ n ^ ":" ^ 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.Cast (v,t) -> "(" ^ pp v l ^ ":" ^ pp t l ^ ")"
     | C.Lambda (b,s,t) ->
        "[" ^ ppname b ^ ":" ^ pp s l ^ "]" ^ pp t ((Some b)::l)
     | C.LetIn (b,s,t) ->
@@ -109,8 +110,8 @@ let rec pp t l =
        UriManager.name_of_uri uri ^ pp_exp_named_subst exp_named_subst l
     | C.MutInd (uri,n,exp_named_subst) ->
        (try
-         match fst(CicEnvironment.get_obj uri CicUniv.empty_ugraph) with
-            C.InductiveDefinition (dl,_,_) ->
+         match fst(CicEnvironment.get_obj CicUniv.empty_ugraph uri) with
+            C.InductiveDefinition (dl,_,_,_) ->
              let (name,_,_,_) = get_nth dl (n+1) in
               name ^ pp_exp_named_subst exp_named_subst l
           | _ -> raise CicPpInternalError
@@ -119,8 +120,8 @@ let rec pp t l =
        )
     | C.MutConstruct (uri,n1,n2,exp_named_subst) ->
        (try
-         match fst(CicEnvironment.get_obj uri CicUniv.empty_ugraph) with
-            C.InductiveDefinition (dl,_,_) ->
+         match fst(CicEnvironment.get_obj CicUniv.empty_ugraph uri) with
+            C.InductiveDefinition (dl,_,_,_) ->
              let (_,_,_,cons) = get_nth dl (n1+1) in
               let (id,_) = get_nth cons n2 in
                id ^ pp_exp_named_subst exp_named_subst l
@@ -132,8 +133,8 @@ let rec pp t l =
        )
     | C.MutCase (uri,n1,ty,te,patterns) ->
        let connames =
-        (match fst(CicEnvironment.get_obj uri CicUniv.empty_ugraph) with
-            C.InductiveDefinition (dl,_,_) ->
+        (match fst(CicEnvironment.get_obj CicUniv.empty_ugraph uri) with
+            C.InductiveDefinition (dl,_,_,_) ->
              let (_,_,_,cons) = get_nth dl (n1+1) in
               List.map (fun (id,_) -> id) cons
           | _ -> raise CicPpInternalError
@@ -217,21 +218,21 @@ let ppobj obj =
  let module C = Cic in
  let module U = UriManager in
   match obj with
-    C.Constant (name, Some t1, t2, params) ->
+    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) ->
+   | 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) ->
+   | 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) ->
+   | C.CurrentProof (name, conjectures, value, ty, params, _) ->
       "Current Proof of " ^ name ^
        "(" ^ String.concat ";" (List.map UriManager.string_of_uri params) ^
        ")" ^ ":\n" ^
@@ -259,9 +260,16 @@ let ppobj obj =
             pp t name_context ^ "\n" ^ i
         ) conjectures "" ^
         "\n" ^ pp value [] ^ " : " ^ pp ty [] 
-   | C.InductiveDefinition (l, params, nparams) ->
+   | C.InductiveDefinition (l, params, nparams, _) ->
       "Parameters = " ^
        String.concat ";" (List.map UriManager.string_of_uri params) ^ "\n" ^
        "NParams = " ^ string_of_int nparams ^ "\n" ^
         List.fold_right (fun x i -> ppinductiveType x ^ i) l ""
 ;;
+
+let ppsort = function
+  | Cic.Prop -> "Prop"
+  | Cic.Set -> "Set"
+  | Cic.Type _ -> "Type"
+  | Cic.CProp -> "CProp"
+