version 0.7.1

[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 abb1b86f37f00295883bacedf9d5fd18cb974edc..effc8a4b58b7450bf71100ea62dc8fc1d97f7610 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicPp.ml
+++ b/helm/ocaml/cic_proof_checking/cicPp.ml
@@ -85,16 +85,18 @@ 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 (Some `Hole) -> "%"
     | C.Implicit _ -> "?"
     | C.Prod (b,s,t) ->
        (match b with
           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) ->
@@ -272,3 +274,116 @@ let ppsort = function
   | Cic.Type _ -> "Type"
   | Cic.CProp -> "CProp"
 
+
+(* MATITA NAMING CONVENTION *)
+
+let check_name ctx name term =
+  let cut_off_name name string_name =
+    let len = String.length name in
+    let len1 = String.length string_name in
+    if len <= len1 then
+      begin
+        let head = String.sub string_name 0 len in
+       if ((String.compare head name)=0) ||
+          ((String.compare head (String.lowercase name))=0) then 
+         begin
+           let diff = len1-len in
+           let tail = String.sub string_name len diff in
+           if ((diff > 0) && (String.rcontains_from tail 0 '_')) then
+             String.sub tail 1 (diff-1)
+           else tail
+         end
+       else string_name
+      end
+    else string_name in
+  let rec check_aux ctx string_name =
+    function
+      | Cic.Rel m -> 
+         (match List.nth ctx (m-1) with
+              Cic.Name name ->
+                cut_off_name name string_name
+            | Cic.Anonymous -> string_name)
+      | Cic.Meta _ -> string_name
+      | Cic.Sort sort -> cut_off_name (ppsort sort) string_name  
+      | Cic.Implicit _ -> string_name
+      | Cic.Cast (te,ty) -> check_aux ctx string_name te
+      | Cic.Prod (name,so,dest) -> 
+         let string_name = check_aux ctx string_name so in
+         check_aux (name::ctx) string_name dest
+      | Cic.Lambda (name,so,dest) -> 
+          let string_name =
+           match name with
+              Cic.Anonymous -> string_name
+            | Cic.Name name -> cut_off_name name string_name in
+          let string_name = check_aux ctx string_name so in
+         check_aux (name::ctx) string_name dest
+      | Cic.LetIn (name,so,dest) -> 
+          let string_name = check_aux ctx string_name so in
+         check_aux (name::ctx) string_name dest
+      | Cic.Appl l ->
+         List.fold_left (check_aux ctx) string_name l
+      | Cic.Var (uri,exp_named_subst) ->
+         let name = UriManager.name_of_uri uri in
+         cut_off_name name string_name
+      | Cic.Const (uri,exp_named_subst) ->
+         let name = UriManager.name_of_uri uri in
+         cut_off_name name string_name
+      | Cic.MutInd (uri,_,exp_named_subst) -> 
+         let name = UriManager.name_of_uri uri in
+         cut_off_name name string_name  
+      | Cic.MutConstruct (uri,n,m,exp_named_subst) ->
+         let name =
+            (match fst(CicEnvironment.get_obj CicUniv.empty_ugraph uri) with
+               Cic.InductiveDefinition (dl,_,_,_) ->
+                 let (_,_,_,cons) = get_nth dl (n+1) in
+                 let (id,_) = get_nth cons m in
+                   id 
+              | _ -> assert false) in
+         cut_off_name name string_name  
+      | Cic.MutCase (_,_,_,te,pl) ->
+         let strig_name = cut_off_name "match" string_name in
+         let string_name = check_aux ctx string_name te in
+          List.fold_right (fun t s -> check_aux ctx s t) pl string_name
+      | Cic.Fix (_,fl) ->
+          let strig_name = cut_off_name "fix" string_name in
+          let names = List.map (fun (name,_,_,_) -> name) fl in
+          let onames =
+            List.rev (List.map (function name -> Cic.Name name) names)
+          in
+          List.fold_right 
+           (fun (_,_,_,bo) s -> check_aux (onames@ctx) s bo) fl string_name
+      | Cic.CoFix (_,fl) ->
+         let strig_name = cut_off_name "cofix" string_name in
+          let names = List.map (fun (name,_,_) -> name) fl in
+          let onames =
+            List.rev (List.map (function name -> Cic.Name name) names)
+          in
+          List.fold_right 
+           (fun (_,_,bo) s -> check_aux (onames@ctx) s bo) fl string_name
+  in
+  if (String.length (check_aux ctx name term) = 0) then true 
+  else false
+
+let rec check_names ctx hyp_names conclusion_name t =
+  match t with
+    | Cic.Prod (name,s,t) -> 
+       (match hyp_names with
+            [] -> check_names (name::ctx) hyp_names conclusion_name t
+          | hd::tl ->
+              if check_name ctx hd s then 
+                check_names (name::ctx) tl conclusion_name t
+              else 
+                check_names (name::ctx) hyp_names conclusion_name t)
+    | _ -> 
+       hyp_names=[] && (check_name ctx conclusion_name t)
+
+let check name term =
+  let names = Str.split (Str.regexp_string "_to_") name in
+  let hyp_names,conclusion_name =
+    match List.rev names with
+       [] -> assert false
+      | hd::tl -> (List.rev tl),hd in
+  check_names [] hyp_names conclusion_name term
+;;
+
+