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=136e9ddaee9150c9eb0acd8d16d7dec0c3986476;hpb=8b9d2632ab7edc7102d16f3857fde02139cef5c2;p=helm.git diff --git a/helm/software/components/cic_proof_checking/cicPp.ml b/helm/software/components/cic_proof_checking/cicPp.ml index 136e9ddae..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,17 +80,41 @@ 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 _ -> "?" @@ -101,8 +126,8 @@ let rec pp t 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) -> - " let " ^ ppname b ^ " \\def " ^ pp s l ^ " in " ^ 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 @@ -139,18 +164,20 @@ let rec pp t l = | C.MutCase (uri,n1,ty,te,patterns) -> 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,ty -> + (fun (id,ty) -> (* this is just an approximation since we do not have reduction yet! *) - let rec count_prods = + let rec count_prods toskip = function - C.Prod (_,_,bo) -> 1 + count_prods bo + C.Prod (_,_,bo) when toskip > 0 -> + count_prods (toskip - 1) bo + | C.Prod (_,_,bo) -> 1 + count_prods 0 bo | _ -> 0 in - id, count_prods ty + id, count_prods paramsno ty ) cons | _ -> raise CicPpInternalError ) @@ -221,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) *) @@ -239,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 ("",[])) @@ -289,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" ^ @@ -316,7 +347,7 @@ let ppsort = function | Cic.Prop -> "Prop" | Cic.Set -> "Set" | Cic.Type _ -> "Type" - | Cic.CProp -> "CProp" + | Cic.CProp _ -> "CProp" (* MATITA NAMING CONVENTION *) @@ -381,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 @@ -389,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 ->