From: Andrea Asperti Date: Thu, 22 Jan 2004 15:27:59 +0000 (+0000) Subject: A few modifications, here and there... X-Git-Tag: V_0_5_1_4~13 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2e062d07e358eb95f0dcbec8fcdfbc2a4fb9ae1f;p=helm.git A few modifications, here and there... --- diff --git a/helm/ocaml/cic_omdoc/cic2acic.ml b/helm/ocaml/cic_omdoc/cic2acic.ml index aa0183dad..d8a442173 100644 --- a/helm/ocaml/cic_omdoc/cic2acic.ml +++ b/helm/ocaml/cic_omdoc/cic2acic.ml @@ -84,7 +84,14 @@ let acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts let fresh_id' = fresh_id seed ids_to_terms ids_to_father_ids in let time1 = Sys.time () in let terms_to_types = - D.double_type_of metasenv context t expectedty + let time0 = Sys.time () in + let prova = CicTypeChecker.type_of_aux' metasenv context t in + let time1 = Sys.time () in + prerr_endline ("*** Fine type_inference:" ^ (string_of_float (time1 -. time0))); + let res = D.double_type_of metasenv context t expectedty in + let time2 = Sys.time () in + prerr_endline ("*** Fine double_type_inference:" ^ (string_of_float (time2 -. time1))); + res in let time2 = Sys.time () in prerr_endline @@ -126,7 +133,7 @@ let acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts (***CSC: patch per provare i tempi CicReduction.whd context (xxx_type_of_aux' metasenv context tt) ; *) Cic.Sort Cic.Type ; - D.expected = None} + D.expected = None} in incr number_new_type_of_aux' ; let innersort = (*XXXXX *) xxx_type_of_aux' metasenv context synthesized (* Cic.Sort Cic.Prop *) in @@ -338,6 +345,54 @@ let acic_of_cic_context metasenv context idrefs t = ids_to_terms, ids_to_father_ids, ids_to_inner_sorts, ids_to_inner_types ;; +let aconjecture_of_conjecture seed ids_to_terms ids_to_father_ids + ids_to_inner_sorts ids_to_inner_types ids_to_hypotheses hypotheses_seed + metasenv (metano,context,goal) = + let acic_of_cic_context = + acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts + ids_to_inner_types metasenv in + let _, acontext,final_idrefs = + (List.fold_right + (fun binding (context, acontext,idrefs) -> + let hid = "h" ^ string_of_int !hypotheses_seed in + Hashtbl.add ids_to_hypotheses hid binding ; + incr hypotheses_seed ; + match binding with + Some (n,Cic.Def (t,None)) -> + let acic = acic_of_cic_context context idrefs t None in + (binding::context), + ((hid,Some (n,Cic.ADef acic))::acontext),(hid::idrefs) + | Some (n,Cic.Decl t) -> + let acic = acic_of_cic_context context idrefs t None in + (binding::context), + ((hid,Some (n,Cic.ADecl acic))::acontext),(hid::idrefs) + | None -> + (* Invariant: "" is never looked up *) + (None::context),((hid,None)::acontext),""::idrefs + | Some (_,Cic.Def (_,Some _)) -> assert false + ) context ([],[],[]) + ) + in + let agoal = acic_of_cic_context context final_idrefs goal None in + (metano,acontext,agoal) +;; + +let asequent_of_sequent (metasenv:Cic.metasenv) (sequent:Cic.conjecture) = + let ids_to_terms = Hashtbl.create 503 in + let ids_to_father_ids = Hashtbl.create 503 in + let ids_to_inner_sorts = Hashtbl.create 503 in + let ids_to_inner_types = Hashtbl.create 503 in + let ids_to_hypotheses = Hashtbl.create 23 in + let hypotheses_seed = ref 0 in + let seed = ref 1 in (* 'i0' is used for the whole sequent *) + let (metano,acontext,agoal) = + aconjecture_of_conjecture seed ids_to_terms ids_to_father_ids + ids_to_inner_sorts ids_to_inner_types ids_to_hypotheses hypotheses_seed + metasenv sequent in + ("i0",metano,acontext,agoal), + ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,ids_to_hypotheses +;; + let acic_object_of_cic_object obj = let module C = Cic in let module E = Eta_fixing in @@ -354,6 +409,9 @@ let acic_object_of_cic_object obj = acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts ids_to_inner_types in let acic_term_of_cic_term' = acic_term_of_cic_term_context' [] [] [] in + let aconjecture_of_conjecture' = aconjecture_of_conjecture seed + ids_to_terms ids_to_father_ids ids_to_inner_sorts ids_to_inner_types + ids_to_hypotheses hypotheses_seed in let aobj = match obj with C.Constant (id,Some bo,ty,params) -> @@ -398,13 +456,17 @@ let acic_object_of_cic_object obj = (i,canonical_context',term') ) conjectures in - let aconjectures = + let aconjectures = List.map (function (i,canonical_context,term) as conjecture -> let cid = "c" ^ string_of_int !conjectures_seed in xxx_add ids_to_conjectures cid conjecture ; incr conjectures_seed ; - let idrefs',revacanonical_context = + let (i,acanonical_context,aterm) + = aconjecture_of_conjecture' conjectures conjecture in + (cid,i,acanonical_context,aterm)) + conjectures' in +(* let idrefs',revacanonical_context = let rec aux context idrefs = function [] -> idrefs,[] @@ -436,14 +498,14 @@ let acic_object_of_cic_object obj = in final_idrefs,(hid,None)::atl in - aux [] [] (List.rev canonical_context) + aux [] [] (List.rev canonical_context) in let aterm = acic_term_of_cic_term_context' conjectures - canonical_context idrefs' term None + canonical_context idrefs' term None in - (cid,i,(List.rev revacanonical_context),aterm) - ) conjectures' in + (cid,i,(List.rev revacanonical_context),aterm) + ) conjectures' in *) let time1 = Sys.time () in let bo' = E.eta_fix conjectures' bo in let ty' = E.eta_fix conjectures' ty in @@ -452,6 +514,7 @@ let acic_object_of_cic_object obj = ("++++++++++ Tempi della eta_fix: "^ string_of_float (time2 -. time1)) ; hashtbl_add_time := 0.0 ; type_of_aux'_add_time := 0.0 ; + DoubleTypeInference.syntactic_equality_add_time := 0.0 ; let abo = acic_term_of_cic_term_context' conjectures' [] [] bo' (Some ty') in let aty = acic_term_of_cic_term_context' conjectures' [] [] ty' None in @@ -462,6 +525,8 @@ let acic_object_of_cic_object obj = ("++++++++++++ Tempi della type_of_aux'_add_time(" ^ string_of_int !number_new_type_of_aux' ^ "): " ^ string_of_float !type_of_aux'_add_time) ; prerr_endline ("++++++++++++ Tempi della type_of_aux'_add_time nella double_type_inference(" ^ string_of_int !DoubleTypeInference.number_new_type_of_aux'_double_work ^ ";" ^ string_of_int !DoubleTypeInference.number_new_type_of_aux'_prop ^ "/" ^ string_of_int !DoubleTypeInference.number_new_type_of_aux' ^ "): " ^ string_of_float !DoubleTypeInference.type_of_aux'_add_time) ; + prerr_endline + ("++++++++++++ Tempi della syntactic_equality_add_time: " ^ string_of_float !DoubleTypeInference.syntactic_equality_add_time) ; prerr_endline ("++++++++++ Tempi della acic_of_cic: " ^ string_of_float (time3 -. time2)) ; prerr_endline @@ -491,3 +556,5 @@ let acic_object_of_cic_object obj = aobj,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,ids_to_inner_types, ids_to_conjectures,ids_to_hypotheses ;; + + diff --git a/helm/ocaml/cic_omdoc/cic2acic.mli b/helm/ocaml/cic_omdoc/cic2acic.mli index b34d34342..4f686da44 100644 --- a/helm/ocaml/cic_omdoc/cic2acic.mli +++ b/helm/ocaml/cic_omdoc/cic2acic.mli @@ -54,3 +54,12 @@ val acic_object_of_cic_object : (Cic.id, anntypes) Hashtbl.t * (* ids_to_inner_types *) (Cic.id, Cic.conjecture) Hashtbl.t * (* ids_to_conjectures *) (Cic.id, Cic.hypothesis) Hashtbl.t (* ids_to_hypotheses *) + +val asequent_of_sequent : + Cic.metasenv -> (* metasenv *) + Cic.conjecture -> (* conjecture *) + Cic.annconjecture * (* annotated conjecture *) + (Cic.id, Cic.term) Hashtbl.t * (* ids_to_terms *) + (Cic.id, Cic.id option) Hashtbl.t * (* ids_to_father_ids *) + (Cic.id, string) Hashtbl.t * (* ids_to_inner_sorts *) + (Cic.id, Cic.hypothesis) Hashtbl.t (* ids_to_hypotheses *) diff --git a/helm/ocaml/cic_omdoc/cic2content.ml b/helm/ocaml/cic_omdoc/cic2content.ml index 614848706..eac04e7aa 100644 --- a/helm/ocaml/cic_omdoc/cic2content.ml +++ b/helm/ocaml/cic_omdoc/cic2content.ml @@ -28,7 +28,7 @@ (* PROJECT HELM *) (* *) (* Andrea Asperti *) -(* 16/62003 *) +(* 16/6/2003 *) (* *) (**************************************************************************) @@ -537,18 +537,37 @@ and acic2content seed ?name ~ids_to_inner_sorts ~ids_to_inner_types t = generate_exact seed t id name ~ids_to_inner_types else raise Not_a_proof | C.AMutCase (id,uri,typeno,ty,te,patterns) -> - let inductive_types = + let inductive_types,noparams = (match CicEnvironment.get_obj uri with Cic.Constant _ -> assert false | Cic.Variable _ -> assert false | Cic.CurrentProof _ -> assert false - | Cic.InductiveDefinition (l,_,_) -> l + | Cic.InductiveDefinition (l,_,n) -> l,n ) in - let (_,_,_,constructors) = List.nth inductive_types typeno in + let (_,_,_,constructors) = List.nth inductive_types typeno in + let name_and_arities = + let rec count_prods = + function + C.Prod (_,_,t) -> 1 + count_prods t + | _ -> 0 in + List.map + (function (n,t) -> Some n,((count_prods t) - noparams)) constructors in + let pp = + let build_proof p (name,arity) = + let rec make_context_and_body c p n = + if n = 0 then c,(aux p) + else + (match p with + Cic.ALambda(idl,vname,s1,t1) -> + let ce = + build_decl_item seed idl vname s1 ~ids_to_inner_sorts in + make_context_and_body (ce::c) t1 (n-1) + | _ -> assert false) in + let context,body = make_context_and_body [] p arity in + K.ArgProof + {body with K.proof_name = name; K.proof_context=context} in + List.map2 build_proof patterns name_and_arities in let teid = get_id te in - let pp = List.map2 - (fun p (name,_) -> (K.ArgProof (aux ~name p))) - patterns constructors in let context,term = (match build_subproofs_and_args @@ -850,6 +869,42 @@ let map_conjectures (id,n,context',ty) ;; +(* map_sequent is similar to map_conjectures, but the for the hid +of the hypothesis, which are preserved instead of generating +fresh ones. We shall have to adopt a uniform policy, soon or later *) + +let map_sequent ((id,n,context,ty):Cic.annconjecture) = + let module K = Content in + let context' = + List.map + (function + (id,None) -> None + | (id,Some (name,Cic.ADecl t)) -> + Some + (* We should call build_decl_item, but we have not computed *) + (* the inner-types ==> we always produce a declaration *) + (`Declaration + { K.dec_name = name_of name; + K.dec_id = id; + K.dec_inductive = false; + K.dec_aref = get_id t; + K.dec_type = t + }) + | (id,Some (name,Cic.ADef t)) -> + Some + (* We should call build_def_item, but we have not computed *) + (* the inner-types ==> we always produce a declaration *) + (`Definition + { K.def_name = name_of name; + K.def_id = id; + K.def_aref = get_id t; + K.def_term = t + }) + ) context + in + (id,n,context',ty) +;; + let rec annobj2content ~ids_to_inner_sorts ~ids_to_inner_types = let module C = Cic in let module K = Content in diff --git a/helm/ocaml/cic_omdoc/cic2content.mli b/helm/ocaml/cic_omdoc/cic2content.mli index 16eb5333f..10ec4b0d1 100644 --- a/helm/ocaml/cic_omdoc/cic2content.mli +++ b/helm/ocaml/cic_omdoc/cic2content.mli @@ -28,3 +28,6 @@ val annobj2content : ids_to_inner_types:(string, Cic2acic.anntypes) Hashtbl.t -> Cic.annobj -> Cic.annterm Content.cobj + +val map_sequent : + Cic.annconjecture -> Cic.annterm Content.conjecture diff --git a/helm/ocaml/cic_omdoc/content.ml b/helm/ocaml/cic_omdoc/content.ml index 748944cdf..ee7b8488d 100644 --- a/helm/ocaml/cic_omdoc/content.ml +++ b/helm/ocaml/cic_omdoc/content.ml @@ -28,7 +28,7 @@ (* PROJECT HELM *) (* *) (* Andrea Asperti *) -(* 16/62003 *) +(* 16/6/2003 *) (* *) (**************************************************************************) diff --git a/helm/ocaml/cic_omdoc/doubleTypeInference.ml b/helm/ocaml/cic_omdoc/doubleTypeInference.ml index f51c00c74..8880ff3f4 100644 --- a/helm/ocaml/cic_omdoc/doubleTypeInference.ml +++ b/helm/ocaml/cic_omdoc/doubleTypeInference.ml @@ -31,6 +31,7 @@ exception WrongUriToMutualInductiveDefinitions of string;; exception ListTooShort;; exception RelToHiddenHypothesis;; +let syntactic_equality_add_time = ref 0.0;; let type_of_aux'_add_time = ref 0.0;; let number_new_type_of_aux'_double_work = ref 0;; let number_new_type_of_aux' = ref 0;; @@ -244,6 +245,15 @@ let syntactic_equality t t' = _ -> false ;; +let xxx_syntactic_equality t t' = + let t1 = Sys.time () in + let res = syntactic_equality t t' in + let t2 = Sys.time () in + syntactic_equality_add_time := !syntactic_equality_add_time +. t2 -. t1 ; + res +;; + + let rec split l n = match (l,n) with (l,0) -> ([], l) @@ -407,7 +417,7 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty = sort_of_prod context (name,s) (sort1,sort2) | C.Lambda (n,s,t) -> (* Let's visit all the subterms that will not be visited later *) - let _ = type_of_aux context s None in + let _ = type_of_aux context s None in let expected_target_type = match expectedty with None -> None @@ -419,7 +429,7 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty = | _ -> assert false in Some ty - in + in let type2 = type_of_aux ((Some (n,(C.Decl s)))::context) t expected_target_type in @@ -433,7 +443,7 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty = let t_typ = (* Checks suppressed *) type_of_aux ((Some (n,(C.Def (s,Some ty))))::context) t None - in + in (* CicSubstitution.subst s t_typ *) if does_not_occur 1 t_typ then (* since [Rel 1] does not occur in typ, substituting any term *) (* in place of [Rel 1] is equivalent to delifting once *) @@ -441,13 +451,25 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty = else C.LetIn (n,s,t_typ) | C.Appl (he::tl) when List.length tl > 0 -> + (* let expected_hetype = (* Inefficient, the head is computed twice. But I know *) - (* of no other solution. *) + (* of no other solution. *) (head_beta_reduce (R.whd context (xxx_type_of_aux' metasenv context he))) - in - let hetype = type_of_aux context he (Some expected_hetype) in + in + let hetype = type_of_aux context he (Some expected_hetype) in + let tlbody_and_type = + let rec aux = + function + _,[] -> [] + | C.Prod (n,s,t),he::tl -> + (he, type_of_aux context he (Some (head_beta_reduce s))):: + (aux (R.whd context (S.subst he t), tl)) + | _ -> assert false + in + aux (expected_hetype, tl) *) + let hetype = R.whd context (type_of_aux context he None) in let tlbody_and_type = let rec aux = function @@ -457,7 +479,7 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty = (aux (R.whd context (S.subst he t), tl)) | _ -> assert false in - aux (expected_hetype, tl) + aux (hetype, tl) in eat_prods context hetype tlbody_and_type | C.Appl _ -> raise (NotWellTyped "Appl: no arguments") @@ -602,7 +624,7 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty = None -> (* No expected type *) {synthesized = synthesized' ; expected = None}, synthesized - | Some ty when syntactic_equality synthesized' ty -> + | Some ty when xxx_syntactic_equality synthesized' ty -> (* The expected type is synthactically equal to *) (* the synthesized type. Let's forget it. *) {synthesized = synthesized' ; expected = None}, synthesized diff --git a/helm/ocaml/cic_omdoc/doubleTypeInference.mli b/helm/ocaml/cic_omdoc/doubleTypeInference.mli index a35c8d6c7..20230e3bb 100644 --- a/helm/ocaml/cic_omdoc/doubleTypeInference.mli +++ b/helm/ocaml/cic_omdoc/doubleTypeInference.mli @@ -6,6 +6,7 @@ exception WrongUriToMutualInductiveDefinitions of string exception ListTooShort exception RelToHiddenHypothesis +val syntactic_equality_add_time: float ref val type_of_aux'_add_time: float ref val number_new_type_of_aux'_double_work: int ref val number_new_type_of_aux': int ref diff --git a/helm/ocaml/cic_omdoc/eta_fixing.ml b/helm/ocaml/cic_omdoc/eta_fixing.ml index c224bcf65..c37911014 100644 --- a/helm/ocaml/cic_omdoc/eta_fixing.ml +++ b/helm/ocaml/cic_omdoc/eta_fixing.ml @@ -214,9 +214,15 @@ let eta_fix metasenv t = | C.Variable _ -> raise ReferenceToVariable | C.CurrentProof (_,_,_,_,params) -> raise RferenceToCurrentProof | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition - ) - in - fix_according_to_type constant_type (C.Const(uri,exp_named_subst)) l'' + ) in + fix_according_to_type + constant_type (C.Const(uri,exp_named_subst)) l'' +(* + let result = fix_according_to_type constant_type (C.Const(uri,exp_named_subst)) l'' in + if not (CicReduction.are_convertible [] appl result) then + (prerr_endline ("prima :" ^(CicPp.ppterm appl)); + prerr_endline ("dopo :" ^(CicPp.ppterm result))); + result *) | _ -> C.Appl l' ) | C.Const (uri,exp_named_subst) -> let exp_named_subst' = @@ -248,7 +254,6 @@ let eta_fix metasenv t = | Cic.InductiveDefinition (l,_,n) -> l,n ) in let (_,_,_,constructors) = List.nth inductive_types tyno in - prerr_endline ("QUI"); let constructor_types = let rec clean_up t = function @@ -294,3 +299,9 @@ let eta_fix metasenv t = + + + + + +