]> matita.cs.unibo.it Git - helm.git/commitdiff
New version of name checking.
authorAndrea Asperti <andrea.asperti@unibo.it>
Fri, 15 Jul 2005 11:11:42 +0000 (11:11 +0000)
committerAndrea Asperti <andrea.asperti@unibo.it>
Fri, 15 Jul 2005 11:11:42 +0000 (11:11 +0000)
helm/ocaml/cic_proof_checking/cicPp.ml

index effc8a4b58b7450bf71100ea62dc8fc1d97f7610..7765328523669ca3ee088371addd99248d14481c 100644 (file)
  * http://cs.unibo.it/helm/.
  *)
 
-(******************************************************************************)
-(*                                                                            *)
-(*                               PROJECT HELM                                 *)
-(*                                                                            *)
-(*                Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>               *)
-(*                                 24/01/2000                                 *)
-(*                                                                            *)
-(* This module implements a very simple Coq-like pretty printer that, given   *)
-(* an object of cic (internal representation) returns a string describing the *)
-(* object in a syntax similar to that of coq                                  *)
-(*                                                                            *)
-(******************************************************************************)
+(*****************************************************************************)
+(*                                                                           *)
+(*                               PROJECT HELM                                *)
+(*                                                                           *)
+(* This module implements a very simple Coq-like pretty printer that, given  *)
+(* an object of cic (internal representation) returns a string describing    *)
+(* the object in a syntax similar to that of coq                             *)
+(*                                                                           *)
+(* It also contains the utility functions to check a name w.r.t the Matita   *)
+(* naming policy                                                             *)
+(*                                                                           *)
+(*****************************************************************************)
 
 exception CicPpInternalError;;
 exception NotEnoughElements;;
@@ -277,91 +277,129 @@ let ppsort = function
 
 (* 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
+let is_prefix prefix string =
+  let len = String.length prefix in
+  let len1 = String.length string in
+  if len <= len1 then
+    begin
+      let head = String.sub string 0 len in
+      if ((String.compare head prefix)=0) ||
+      ((String.compare head (String.lowercase prefix))=0) then 
+       begin
+         let diff = len1-len in
+         let tail = String.sub string len diff in
+         if ((diff > 0) && (String.rcontains_from tail 0 '_')) then
+           Some (String.sub tail 1 (diff-1))
+           else Some 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 None
+    end
+  else None
+
+let remove_prefix prefix (last,string) =
+  if string = "" then (last,string)
+  else 
+    match is_prefix prefix string with
+      None ->
+       if last <> "" then 
+         match is_prefix last prefix with
+           None -> (last,string)
+         | Some _ ->
+              (match is_prefix prefix (last^string) with
+               None -> (last,string)
+             | Some tail -> (prefix,tail))
+       else (last,string)
+    | Some tail -> (prefix, tail)
+       
+let legal_suffix string = 
+  if string = "" then true else
+  begin
+    let legal_s = Str.regexp "_?\\([0-9]+\\|r\\|l\\|'\\|\"\\)" in
+    (Str.string_match legal_s string 0) && (Str.matched_string string = string)
+  end
+
+(** check if a prefix of string_name is legal for term and returns the tail.
+    chec_rec cannot fail: at worst it return string_name.
+    The algorithm is greedy, but last contains the last name matched, providing
+    a one slot buffer. 
+    string_name is here a pair (last,string_name).*)
+
+let rec check_rec ctx string_name =
+  function
+    | Cic.Rel m -> 
+       (match List.nth ctx (m-1) with
+         Cic.Name name ->
+           remove_prefix name string_name
+       | Cic.Anonymous -> string_name)
+    | Cic.Meta _ -> string_name
+    | Cic.Sort sort -> remove_prefix (ppsort sort) string_name  
+    | Cic.Implicit _ -> string_name
+    | Cic.Cast (te,ty) -> check_rec ctx string_name te
+    | Cic.Prod (name,so,dest) -> 
+       let l_string_name = check_rec ctx string_name so in
+       check_rec (name::ctx) string_name dest
+    | Cic.Lambda (name,so,dest) -> 
+        let string_name =
+          match name with
+            Cic.Anonymous -> string_name
+          | Cic.Name name -> remove_prefix name string_name in
+        let l_string_name = check_rec ctx string_name so in
+       check_rec (name::ctx) l_string_name dest
+    | Cic.LetIn (name,so,dest) -> 
+        let string_name = check_rec ctx string_name so in
+       check_rec (name::ctx) string_name dest
+    | Cic.Appl l ->
+       List.fold_left (check_rec ctx) string_name l
+    | Cic.Var (uri,exp_named_subst) ->
+       let name = UriManager.name_of_uri uri in
+       remove_prefix name string_name
+    | Cic.Const (uri,exp_named_subst) ->
+       let name = UriManager.name_of_uri uri in
+       remove_prefix name string_name
+    | Cic.MutInd (uri,_,exp_named_subst) -> 
+       let name = UriManager.name_of_uri uri in
+       remove_prefix 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
+       remove_prefix name string_name  
+    | Cic.MutCase (_,_,_,te,pl) ->
+       let strig_name = remove_prefix "match" string_name in
+       let string_name = check_rec ctx string_name te in
+        List.fold_right (fun t s -> check_rec ctx s t) pl string_name
+    | Cic.Fix (_,fl) ->
+        let strig_name = remove_prefix "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_rec (onames@ctx) s bo) fl string_name
+    | Cic.CoFix (_,fl) ->
+       let strig_name = remove_prefix "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_rec (onames@ctx) s bo) fl string_name
+
+let check_name ?(allow_suffix=false) ctx name term =
+  let (_,tail) = check_rec ctx ("",name) term in
+  if (not allow_suffix) then (String.length tail = 0) 
+  else legal_suffix tail
+
+let check_elim ctx conclusion_name =
+  let elim = Str.regexp "_elim\\|_case" in
+  if (Str.string_match elim conclusion_name 0) then
+    let len = String.length conclusion_name in
+    let tail = String.sub conclusion_name 5 (len-5) in
+    legal_suffix tail
   else false
 
 let rec check_names ctx hyp_names conclusion_name t =
@@ -374,15 +412,47 @@ let rec check_names ctx hyp_names conclusion_name t =
                 check_names (name::ctx) tl conclusion_name t
               else 
                 check_names (name::ctx) hyp_names conclusion_name t)
+    | Cic.Appl ((Cic.Rel n)::args) -> 
+       (match hyp_names with
+         | [] ->
+             (check_name ~allow_suffix:true ctx conclusion_name t) ||
+              (check_elim ctx conclusion_name)
+         | [what_to_elim] ->   
+              (* what to elim could be an argument 
+                 of the predicate: e.g. leb_elim *)
+             let (last,tail) = 
+               List.fold_left (check_rec ctx) ("",what_to_elim) args in
+              (tail = "" && check_elim ctx conclusion_name)
+         | _ -> false)
+    | Cic.MutCase  (_,_,Cic.Lambda(name,so,ty),te,_) ->
+       (match hyp_names with
+         | [] ->
+               (match is_prefix "match" conclusion_name with
+                  None -> check_name ~allow_suffix:true ctx conclusion_name t
+              | Some tail -> check_name ~allow_suffix:true ctx tail t)
+         | [what_to_match] ->   
+              (* what to match could be the term te or its type so; in this case the
+                 conclusion name should match ty *)
+             check_name ~allow_suffix:true (name::ctx) conclusion_name ty &&
+              (check_name ctx what_to_match te || check_name ctx what_to_match so)
+         | _ -> false)
     | _ -> 
-       hyp_names=[] && (check_name ctx conclusion_name t)
+       hyp_names=[] && check_name ~allow_suffix:true 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
+      | hd::tl -> 
+          let elim = Str.regexp "_elim\\|_case" in
+          let len = String.length hd in
+          try 
+           let pos = Str.search_backward elim hd len in
+           let hyp = String.sub hd 0 pos in
+           let concl = String.sub hd pos (len-pos) in
+           List.rev (hyp::tl),concl
+          with Not_found -> (List.rev tl),hd in
   check_names [] hyp_names conclusion_name term
 ;;