X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_proof_checking%2FcicPp.ml;h=97213404e7244a0b8c082b68b44f1d12bf14d53c;hb=11b2157bacf59cfc561c2ef6f92ee41ee2c1a006;hp=954134584b69db831d0d060cc0ed2bd301b4bdb0;hpb=55b82bd235d82ff7f0a40d980effe1efde1f5073;p=helm.git

diff --git a/helm/software/components/cic_proof_checking/cicPp.ml b/helm/software/components/cic_proof_checking/cicPp.ml
index 954134584..97213404e 100644
--- a/helm/software/components/cic_proof_checking/cicPp.ml
+++ b/helm/software/components/cic_proof_checking/cicPp.ml
@@ -62,6 +62,7 @@ let rec get_nth l n =
 (* pretty-prints a term t of cic in an environment l where l is a list of  *)
 (* identifier names used to resolve DeBrujin indexes. The head of l is the *)
 (* name associated to the greatest DeBrujin index in t                     *)
+let pp ?metasenv =
 let rec pp t l =
  let module C = Cic in
    match t with
@@ -79,30 +80,54 @@ let rec pp t l =
     | 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 " ; "
-         (List.rev_map (function None -> "_" | Some t -> pp t l) l1) ^
-        "]"
+       (match metasenv with
+           None ->
+            "?" ^ (string_of_int n) ^ "[" ^ 
+             String.concat " ; "
+              (List.rev_map (function None -> "_" | Some t -> pp t l) l1) ^
+             "]"
+         | Some metasenv ->
+            try
+             let _,context,_ = CicUtil.lookup_meta n metasenv in
+              "?" ^ (string_of_int n) ^ "[" ^ 
+               String.concat " ; "
+                (List.rev
+                  (List.map2
+                    (fun x y ->
+                      match x,y with
+                         _, None
+                       | None, _ -> "_"
+                       | Some _, Some t -> pp t l
+                    ) context l1)) ^
+               "]"
+            with
+	      CicUtil.Meta_not_found _ 
+            | Invalid_argument _ ->
+              "???" ^ (string_of_int n) ^ "[" ^ 
+               String.concat " ; "
+                (List.rev_map (function None -> "_" | Some t -> pp t l) l1) ^
+               "]"
+       )
     | C.Sort s ->
        (match s with
            C.Prop  -> "Prop"
          | C.Set   -> "Set"
          | C.Type _ -> "Type"
          (*| C.Type u -> ("Type" ^ CicUniv.string_of_universe u)*)
-	 | C.CProp -> "CProp" 
+	 | 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.Name n -> "(\\forall " ^ n ^ ":" ^ pp s l ^ "." ^ pp t ((Some b)::l) ^ ")"
+        | C.Anonymous -> "(" ^ pp s l ^ "\\to " ^ pp t ((Some b)::l) ^ ")"
        )
     | C.Cast (v,t) -> "(" ^ pp v l ^ ":" ^ pp t l ^ ")"
     | C.Lambda (b,s,t) ->
        "(\\lambda " ^ ppname b ^ ":" ^ pp s l ^ "." ^ pp t ((Some b)::l) ^ ")"
-    | C.LetIn (b,s,t) ->
-       "[" ^ ppname b ^ ":=" ^ pp s l ^ "]" ^ pp t ((Some b)::l)
+    | C.LetIn (b,s,ty,t) ->
+       " let " ^ ppname b ^ ": " ^ pp ty l ^ " \\def " ^ pp s l ^ " in " ^ pp t ((Some b)::l)
     | C.Appl li ->
        "(" ^
        (List.fold_right
@@ -119,7 +144,8 @@ let rec pp t l =
               name ^ pp_exp_named_subst exp_named_subst l
           | _ -> raise CicPpInternalError
         with
-         _ -> UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (n + 1)
+           Sys.Break as exn -> raise exn
+         | _ -> UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (n + 1)
        )
     | C.MutConstruct (uri,n1,n2,exp_named_subst) ->
        (try
@@ -130,35 +156,66 @@ let rec pp t l =
                id ^ pp_exp_named_subst exp_named_subst l
           | _ -> raise CicPpInternalError
         with
-         _ ->
+           Sys.Break as exn -> raise exn
+         | _ ->
           UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (n1 + 1) ^ "/" ^
            string_of_int n2
        )
     | C.MutCase (uri,n1,ty,te,patterns) ->
-       let connames =
+       let connames_and_argsno =
         (match fst(CicEnvironment.get_obj CicUniv.empty_ugraph uri) with
-            C.InductiveDefinition (dl,_,_,_) ->
+            C.InductiveDefinition (dl,_,paramsno,_) ->
              let (_,_,_,cons) = get_nth dl (n1+1) in
-              List.map (fun (id,_) -> id) cons
+              List.map
+               (fun (id,ty) ->
+                 (* this is just an approximation since we do not have
+                    reduction yet! *)
+                 let rec count_prods toskip =
+                  function
+                     C.Prod (_,_,bo) when toskip > 0 ->
+                      count_prods (toskip - 1) bo
+                   | C.Prod (_,_,bo) -> 1 + count_prods 0 bo
+                   | _ -> 0
+                 in
+                  id, count_prods paramsno ty
+               ) cons
           | _ -> raise CicPpInternalError
         )
        in
-        let connames_and_patterns =
+        let connames_and_argsno_and_patterns =
          let rec combine =
             function
                [],[] -> []
-             | [],l -> List.map (fun x -> "???",Some x) l
-             | l,[] -> List.map (fun x -> x,None) l
-             | x::tlx,y::tly -> (x,Some y)::(combine (tlx,tly))
+             | [],l -> List.map (fun x -> "???",0,Some x) l
+             | l,[] -> List.map (fun (x,no) -> x,no,None) l
+             | (x,no)::tlx,y::tly -> (x,no,Some y)::(combine (tlx,tly))
          in
-          combine (connames,patterns)
+          combine (connames_and_argsno,patterns)
         in
-        "\n<" ^ pp ty l ^ ">Cases " ^ pp te l ^ " of " ^
-          List.fold_right
-           (fun (x,y) i -> "\n " ^ x ^ " => " ^
-             (match y with None -> "" | Some y -> pp y l) ^ i)
-           connames_and_patterns "" ^
-          "\nend"
+         "\nmatch " ^ pp te l ^ " return " ^ pp ty l ^ " with \n [ " ^
+          (String.concat "\n | "
+           (List.map
+            (fun (x,argsno,y) ->
+              let rec aux argsno l =
+               function
+                  Cic.Lambda (name,ty,bo) when argsno > 0 ->
+                   let args,res = aux (argsno - 1) (Some name::l) bo in
+                    ("(" ^ (match name with C.Anonymous -> "_" | C.Name s -> s)^
+                     ":" ^ pp ty l ^ ")")::args, res
+                | t when argsno = 0 -> [],pp t l
+                | t -> ["{" ^ string_of_int argsno ^ " args missing}"],pp t l
+              in
+               let pattern,body =
+                match y with
+                   None -> x,""
+                 | Some y when argsno = 0 -> x,pp y l
+                 | Some y ->
+                    let args,body = aux argsno l y in
+                     "(" ^ x ^ " " ^ String.concat " " args ^ ")",body
+               in
+                pattern ^ " => " ^ body
+            ) connames_and_argsno_and_patterns)) ^
+          "\n]"
     | C.Fix (no, funs) ->
        let snames = List.map (fun (name,_,_,_) -> name) funs in
         let names =
@@ -191,10 +248,12 @@ and pp_exp_named_subst exp_named_subst l =
      (function (uri,t) -> UriManager.name_of_uri uri ^ " \\Assign " ^ pp t l)
      exp_named_subst
    ) ^ "]"
+in
+ pp
 ;;
 
-let ppterm t =
- pp t []
+let ppterm ?metasenv t =
+ pp ?metasenv t []
 ;;
 
 (* ppinductiveType (typename, inductive, arity, cons)                       *)
@@ -209,20 +268,18 @@ let ppinductiveType (typename, inductive, arity, cons) =
    cons ""
 ;;
 
-let ppcontext ?(sep = "\n") context =
+let ppcontext ?metasenv ?(sep = "\n") context =
  let separate s = if s = "" then "" else s ^ sep in
  fst (List.fold_right 
    (fun context_entry (i,name_context) ->
      match context_entry with
         Some (n,Cic.Decl t) ->
          Printf.sprintf "%s%s : %s" (separate i) (ppname n)
-          (pp t name_context), (Some n)::name_context
+          (pp ?metasenv t name_context), (Some n)::name_context
       | Some (n,Cic.Def (bo,ty)) ->
          Printf.sprintf "%s%s : %s := %s" (separate i) (ppname n)
-          (match ty with
-              None -> "_"
-            | Some ty -> pp ty name_context)
-          (pp bo name_context), (Some n)::name_context
+          (pp ?metasenv ty name_context)
+          (pp ?metasenv bo name_context), (Some n)::name_context
        | None ->
           Printf.sprintf "%s_ :? _" (separate i), None::name_context
     ) context ("",[]))
@@ -259,22 +316,26 @@ let ppobj obj =
 	          (fun context_entry (i,name_context) ->
 	            (match context_entry with
 	                Some (n,C.Decl at) ->
-                   (separate i) ^
-                     ppname n ^ ":" ^ pp at name_context ^ " ",
-                      (Some n)::name_context
-	              | Some (n,C.Def (at,None)) ->
-                   (separate i) ^
-                     ppname n ^ ":= " ^ pp at name_context ^ " ",
-                      (Some n)::name_context
-                | None ->
-                   (separate i) ^ "_ :? _ ", None::name_context
-                | _ -> assert false)
+                         (separate i) ^
+                           ppname n ^ ":" ^
+                            pp ~metasenv:conjectures at name_context ^ " ",
+                            (Some n)::name_context
+                      | Some (n,C.Def (at,aty)) ->
+                         (separate i) ^
+                           ppname n ^ ": " ^
+                            pp ~metasenv:conjectures aty name_context ^
+                            ":= " ^ pp ~metasenv:conjectures
+                            at name_context ^ " ",
+                            (Some n)::name_context
+                      | None ->
+                         (separate i) ^ "_ :? _ ", None::name_context)
             ) context ("",[])
           in
            conjectures' ^ " |- " ^ "?" ^ (string_of_int n) ^ ": " ^
-            pp t name_context ^ "\n" ^ i
+            pp ~metasenv:conjectures t name_context ^ "\n" ^ i
         ) conjectures "" ^
-        "\n" ^ pp value [] ^ " : " ^ pp ty [] 
+        "\n" ^ pp ~metasenv:conjectures value [] ^ " : " ^
+          pp ~metasenv:conjectures ty [] 
    | C.InductiveDefinition (l, params, nparams, _) ->
       "Parameters = " ^
        String.concat ";" (List.map UriManager.string_of_uri params) ^ "\n" ^
@@ -286,7 +347,7 @@ let ppsort = function
   | Cic.Prop -> "Prop"
   | Cic.Set -> "Set"
   | Cic.Type _ -> "Type"
-  | Cic.CProp -> "CProp"
+  | Cic.CProp _ -> "CProp"
 
 
 (* MATITA NAMING CONVENTION *)
@@ -311,11 +372,6 @@ let is_prefix prefix string =
   else None
 
 let remove_prefix prefix (last,string) =
-  if prefix="append" then
-    begin 
-      prerr_endline last;
-      prerr_endline string;
-    end;
   if string = "" then (last,string)
   else 
     match is_prefix prefix string with
@@ -356,7 +412,7 @@ let rec check_rec ctx 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
+	check_rec (name::ctx) l_string_name dest
     | Cic.Lambda (name,so,dest) -> 
         let string_name =
           match name with
@@ -364,7 +420,7 @@ let rec check_rec ctx 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) -> 
+    | 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 ->
@@ -388,11 +444,11 @@ let rec check_rec ctx string_name =
 	  | _ -> assert false) in
 	remove_prefix name string_name  
     | Cic.MutCase (_,_,_,te,pl) ->
-	let strig_name = remove_prefix "match" string_name in
+	let string_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 string_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)
@@ -400,7 +456,7 @@ let rec check_rec ctx string_name =
         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 string_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)
@@ -459,8 +515,6 @@ let rec check_names ctx hyp_names conclusion_name t =
 	hyp_names=[] && check_name ~allow_suffix:true ctx conclusion_name t
 
 let check name term =
-(*  prerr_endline name;
-  prerr_endline (ppterm term); *)
   let names = Str.split (Str.regexp_string "_to_") name in
   let hyp_names,conclusion_name =
     match List.rev names with