X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicPp.ml;h=effc8a4b58b7450bf71100ea62dc8fc1d97f7610;hb=12cc5b2b8e7f7bb0b5e315094b008a293a4df6b1;hp=a8d9eaa0bdd87e4ef67c60611e4c8e314b0f53cd;hpb=296b163c8a2b09a6f87cbab15c2016de92fc8e70;p=helm.git diff --git a/helm/ocaml/cic_proof_checking/cicPp.ml b/helm/ocaml/cic_proof_checking/cicPp.ml index a8d9eaa0b..effc8a4b5 100644 --- a/helm/ocaml/cic_proof_checking/cicPp.ml +++ b/helm/ocaml/cic_proof_checking/cicPp.ml @@ -41,7 +41,7 @@ exception NotEnoughElements;; (* Utility functions *) -let string_of_name = +let ppname = function Cic.Name s -> s | Cic.Anonymous -> "_" @@ -69,7 +69,7 @@ let rec pp t l = (match get_nth l n with Some (C.Name s) -> s | Some C.Anonymous -> "__" ^ string_of_int n - | _ -> raise CicPpInternalError + | None -> "_hidden_" ^ string_of_int n ) with NotEnoughElements -> string_of_int (List.length l - n) @@ -79,26 +79,28 @@ let rec pp t l = | C.Meta (n,l1) -> "?" ^ (string_of_int n) ^ "[" ^ String.concat " ; " - (List.map (function None -> "_" | Some t -> pp t l) l1) ^ + (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 _ -> "Type" + (*| C.Type u -> ("Type" ^ CicUniv.string_of_universe u)*) | C.CProp -> "CProp" ) - | C.Implicit -> "?" + | 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) -> - "[" ^ string_of_name b ^ ":" ^ pp s l ^ "]" ^ pp t ((Some b)::l) + "[" ^ ppname b ^ ":" ^ pp s l ^ "]" ^ pp t ((Some b)::l) | C.LetIn (b,s,t) -> - "[" ^ string_of_name b ^ ":=" ^ pp s l ^ "]" ^ pp t ((Some b)::l) + "[" ^ ppname b ^ ":=" ^ pp s l ^ "]" ^ pp t ((Some b)::l) | C.Appl li -> "(" ^ (List.fold_right @@ -109,8 +111,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 CicEnvironment.get_obj uri 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 +121,8 @@ let rec pp t l = ) | C.MutConstruct (uri,n1,n2,exp_named_subst) -> (try - match CicEnvironment.get_obj uri 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 +134,8 @@ let rec pp t l = ) | C.MutCase (uri,n1,ty,te,patterns) -> let connames = - (match CicEnvironment.get_obj uri 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 @@ -193,27 +195,45 @@ let ppinductiveType (typename, inductive, arity, cons) = cons "" ;; +let ppcontext ?(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 + | 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 + | None -> + Printf.sprintf "%s_ :? _" (separate i), None::name_context + ) context ("",[])) + (* ppobj obj returns a string with describing the cic object obj in a syntax *) (* similar to the one used by Coq *) 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" ^ @@ -226,11 +246,11 @@ let ppobj obj = (match context_entry with Some (n,C.Decl at) -> (separate i) ^ - string_of_name n ^ ":" ^ pp at name_context ^ " ", + ppname n ^ ":" ^ pp at name_context ^ " ", (Some n)::name_context | Some (n,C.Def (at,None)) -> (separate i) ^ - string_of_name n ^ ":= " ^ pp at name_context ^ " ", + ppname n ^ ":= " ^ pp at name_context ^ " ", (Some n)::name_context | None -> (separate i) ^ "_ :? _ ", None::name_context @@ -241,9 +261,129 @@ 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" + + +(* 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 +;; + +