From cc23f034c9419186602d9250456241f2eba90d7c Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 11 Mar 2008 22:02:58 +0000 Subject: [PATCH] Very experimental commit: the type of the source is now required in LetIns and Defs. This is a back-porting from the new generation kernel. TODO: a) debug some failing examples (paramodulation) b) port the code by Ferruccio c) do something for Coq files (that are now rejected) --- .../components/acic_content/acic2content.ml | 48 ++++++----- .../components/acic_content/cicNotationPp.ml | 7 +- .../acic_content/cicNotationUtil.ml | 8 +- .../components/acic_content/content.ml | 3 +- .../components/acic_content/content.mli | 3 +- .../components/acic_content/content2cic.ml | 19 +++-- .../acic_content/termAcicContent.ml | 4 +- .../acic_procedural/acic2Procedural.ml | 5 +- .../acic_procedural/proceduralConversion.ml | 28 +++---- .../acic_procedural/proceduralHelpers.ml | 16 ++-- .../acic_procedural/proceduralOptimizer.ml | 39 +++++---- helm/software/components/cic/cic.ml | 8 +- helm/software/components/cic/cicInspect.ml | 11 +-- helm/software/components/cic/cicParser.ml | 13 +-- helm/software/components/cic/cicUtil.ml | 38 +++++---- helm/software/components/cic/deannotate.ml | 7 +- helm/software/components/cic/unshare.ml | 3 +- helm/software/components/cic_acic/cic2Xml.ml | 14 ++-- helm/software/components/cic_acic/cic2acic.ml | 53 ++++++------ .../cic_acic/doubleTypeInference.ml | 35 ++++---- .../components/cic_acic/eta_fixing.ml | 12 ++- .../cic_disambiguation/disambiguate.ml | 12 +-- .../cic_exportation/cicExportation.ml | 26 +++--- .../cic_proof_checking/cicMiniReduction.ml | 2 +- .../components/cic_proof_checking/cicPp.ml | 35 ++++---- .../cic_proof_checking/cicReduction.ml | 17 ++-- .../cic_proof_checking/cicSubstitution.ml | 11 ++- .../cic_proof_checking/cicTypeChecker.ml | 48 ++++++----- .../cic_proof_checking/cicUnivUtils.ml | 2 +- .../cic_proof_checking/freshNamesGenerator.ml | 20 +++-- .../cic_unification/cicMetaSubst.ml | 36 ++++---- .../components/cic_unification/cicRefine.ml | 70 ++++++++-------- .../components/cic_unification/cicReplace.ml | 6 +- .../cic_unification/cicUnification.ml | 12 +-- .../content_pres/termContentPres.ml | 7 +- .../metadata/metadataConstraints.ml | 14 ++-- .../components/metadata/metadataExtractor.ml | 4 +- helm/software/components/tactics/auto.ml | 13 +-- helm/software/components/tactics/fourierR.ml | 6 +- .../tactics/paramodulation/equality.ml | 42 +++++++--- .../tactics/paramodulation/saturation.ml | 5 +- .../tactics/paramodulation/subst.ml | 2 +- .../tactics/paramodulation/utils.ml | 6 +- .../components/tactics/primitiveTactics.ml | 52 +++--------- .../components/tactics/primitiveTactics.mli | 4 - .../components/tactics/proofEngineHelpers.ml | 82 +++++++++---------- .../components/tactics/proofEngineHelpers.mli | 2 +- .../tactics/proofEngineReduction.ml | 22 ++--- .../tactics/proofEngineStructuralRules.ml | 20 +---- .../components/tactics/reductionTactics.ml | 24 +----- helm/software/components/tactics/setoids.ml | 2 +- helm/software/components/tactics/universe.ml | 5 +- .../components/tactics/variousTactics.ml | 8 +- helm/software/matita/matitaScript.ml | 4 +- 54 files changed, 497 insertions(+), 498 deletions(-) diff --git a/helm/software/components/acic_content/acic2content.ml b/helm/software/components/acic_content/acic2content.ml index 69a1f632d..b10464bda 100644 --- a/helm/software/components/acic_content/acic2content.ml +++ b/helm/software/components/acic_content/acic2content.ml @@ -78,7 +78,7 @@ let rec occur uri = | C.Prod (_,s,t) -> (occur uri s) or (occur uri t) | C.Cast (te,ty) -> (occur uri te) | C.Lambda (_,s,t) -> (occur uri s) or (occur uri t) (* or false ?? *) - | C.LetIn (_,s,t) -> (occur uri s) or (occur uri t) + | C.LetIn (_,s,ty,t) -> (occur uri s) or (occur uri ty) or (occur uri t) | C.Appl l -> List.fold_left (fun b a -> @@ -103,7 +103,7 @@ let get_id = | C.AProd (id,_,_,_) -> id | C.ACast (id,_,_) -> id | C.ALambda (id,_,_,_) -> id - | C.ALetIn (id,_,_,_) -> id + | C.ALetIn (id,_,_,_,_) -> id | C.AAppl (id,_) -> id | C.AConst (id,_,_) -> id | C.AMutInd (id,_,_,_) -> id @@ -145,7 +145,7 @@ let test_for_lifting ~ids_to_inner_types ~ids_to_inner_sorts= ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized; true; with Not_found -> false) - | C.ALetIn (id,_,_,_) -> + | C.ALetIn (id,_,_,_,_) -> (try ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized; true; @@ -274,7 +274,7 @@ let generate_exact seed t id name ~ids_to_inner_types = } ;; -let generate_intros_let_tac seed id n s is_intro inner_proof name ~ids_to_inner_types = +let generate_intros_let_tac seed id n s ty inner_proof name ~ids_to_inner_types = let module C2A = Cic2acic in let module C = Cic in let module K = Content in @@ -294,8 +294,9 @@ let generate_intros_let_tac seed id n s is_intro inner_proof name ~ids_to_inner_ (match inner_proof.K.proof_conclude.K.conclude_conclusion with None -> None | Some t -> - if is_intro then Some (C.AProd ("gen"^id,n,s,t)) - else Some (C.ALetIn ("gen"^id,n,s,t))) + match ty with + None -> Some (C.AProd ("gen"^id,n,s,t)) + | Some ty -> Some (C.ALetIn ("gen"^id,n,s,ty,t))) }; } ;; @@ -459,7 +460,7 @@ let rec build_subproofs_and_args ?(headless=false) seed context metasenv l ~ids_ and -build_def_item seed context metasenv id n t ~ids_to_inner_sorts ~ids_to_inner_types = +build_def_item seed context metasenv id n t ty ~ids_to_inner_sorts ~ids_to_inner_types = let module K = Content in try let sort = Hashtbl.find ids_to_inner_sorts id in @@ -473,7 +474,8 @@ build_def_item seed context metasenv id n t ~ids_to_inner_sorts ~ids_to_inner_ty { K.def_name = name_of n; K.def_id = gen_id definition_prefix seed; K.def_aref = id; - K.def_term = t + K.def_term = t; + K.def_type = ty } with Not_found -> assert false @@ -528,14 +530,16 @@ and acic2content seed context metasenv ?name ~ids_to_inner_sorts ~ids_to_inner_t proof'.K.proof_context } in - generate_intros_let_tac seed id n s true proof'' name ~ids_to_inner_types + generate_intros_let_tac seed id n s None proof'' name ~ids_to_inner_types else raise Not_a_proof - | C.ALetIn (id,n,s,t) -> + | C.ALetIn (id,n,s,ty,t) -> let sort = Hashtbl.find ids_to_inner_sorts id in if sort = `Prop then - let proof = (* XXX TIPAMI!!! *) - aux ((Some (n,Cic.Def (Deannotate.deannotate_term s,None)))::context) t + let proof = + aux + ((Some (n, + Cic.Def (Deannotate.deannotate_term s,Deannotate.deannotate_term ty)))::context) t in let proof' = if proof.K.proof_conclude.K.conclude_method = "Intros+LetTac" then @@ -547,12 +551,12 @@ and acic2content seed context metasenv ?name ~ids_to_inner_sorts ~ids_to_inner_t { proof' with K.proof_name = None; K.proof_context = - ((build_def_item seed context metasenv (get_id s) n s ids_to_inner_sorts + ((build_def_item seed context metasenv (get_id s) n s ty ids_to_inner_sorts ids_to_inner_types):> Cic.annterm K.in_proof_context_element) ::proof'.K.proof_context; } in - generate_intros_let_tac seed id n s false proof'' name ~ids_to_inner_types + generate_intros_let_tac seed id n s (Some ty) proof'' name ~ids_to_inner_types else raise Not_a_proof | C.AAppl (id,li) -> @@ -1040,7 +1044,7 @@ let map_conjectures K.dec_aref = get_id t; K.dec_type = t }) - | (id,Some (name,Cic.ADef t)) -> + | (id,Some (name,Cic.ADef (t,ty))) -> Some (* We should call build_def_item, but we have not computed *) (* the inner-types ==> we always produce a declaration *) @@ -1048,7 +1052,8 @@ let map_conjectures { K.def_name = name_of name; K.def_id = gen_id definition_prefix seed; K.def_aref = get_id t; - K.def_term = t + K.def_term = t; + K.def_type = ty }) ) context in @@ -1076,7 +1081,7 @@ let map_sequent ((id,n,context,ty):Cic.annconjecture) = K.dec_aref = get_id t; K.dec_type = t }) - | (id,Some (name,Cic.ADef t)) -> + | (id,Some (name,Cic.ADef (t,ty))) -> Some (* We should call build_def_item, but we have not computed *) (* the inner-types ==> we always produce a declaration *) @@ -1084,7 +1089,8 @@ let map_sequent ((id,n,context,ty):Cic.annconjecture) = { K.def_name = name_of name; K.def_id = id; K.def_aref = get_id t; - K.def_term = t + K.def_term = t; + K.def_type = ty }) ) context in @@ -1106,12 +1112,12 @@ let rec annobj2content ~ids_to_inner_sorts ~ids_to_inner_types = `Def (K.Const,ty, build_def_item seed [] (Deannotate.deannotate_conjectures conjectures) - (get_id bo) (C.Name n) bo + (get_id bo) (C.Name n) bo ty ~ids_to_inner_sorts ~ids_to_inner_types)) | C.AConstant (_,_,n,Some bo,ty,params,_) -> (gen_id object_prefix seed, params, None, `Def (K.Const,ty, - build_def_item seed [] [] (get_id bo) (C.Name n) bo + build_def_item seed [] [] (get_id bo) (C.Name n) bo ty ~ids_to_inner_sorts ~ids_to_inner_types)) | C.AConstant (id,_,n,None,ty,params,_) -> (gen_id object_prefix seed, params, None, @@ -1121,7 +1127,7 @@ let rec annobj2content ~ids_to_inner_sorts ~ids_to_inner_types = | C.AVariable (_,n,Some bo,ty,params,_) -> (gen_id object_prefix seed, params, None, `Def (K.Var,ty, - build_def_item seed [] [] (get_id bo) (C.Name n) bo + build_def_item seed [] [] (get_id bo) (C.Name n) bo ty ~ids_to_inner_sorts ~ids_to_inner_types)) | C.AVariable (id,n,None,ty,params,_) -> (gen_id object_prefix seed, params, None, diff --git a/helm/software/components/acic_content/cicNotationPp.ml b/helm/software/components/acic_content/cicNotationPp.ml index 4bd2f93ed..236b98507 100644 --- a/helm/software/components/acic_content/cicNotationPp.ml +++ b/helm/software/components/acic_content/cicNotationPp.ml @@ -115,9 +115,12 @@ let rec pp_term ?(pp_parens = true) t = (match typ with None -> "" | Some t -> sprintf " return %s" (pp_term t)) (pp_patterns patterns) | Ast.Cast (t1, t2) -> sprintf "(%s: %s)" (pp_term ~pp_parens:true t1) (pp_term ~pp_parens:true t2) - | Ast.LetIn (var, t1, t2) -> - sprintf "let %s \\def %s in %s" (pp_capture_variable pp_term var) (pp_term ~pp_parens:true t1) + | Ast.LetIn ((var,t2), t1, t3) -> + let t2 = match t2 with None -> Ast.Implicit | Some t -> t in + sprintf "let %s : %s \\def %s in %s" (pp_term var) (pp_term ~pp_parens:true t2) + (pp_term ~pp_parens:true t1) + (pp_term ~pp_parens:true t3) | Ast.LetRec (kind, definitions, term) -> let rec get_guard i = function | [] -> (*assert false*) Ast.Implicit diff --git a/helm/software/components/acic_content/cicNotationUtil.ml b/helm/software/components/acic_content/cicNotationUtil.ml index 99aafa440..51acf758f 100644 --- a/helm/software/components/acic_content/cicNotationUtil.ml +++ b/helm/software/components/acic_content/cicNotationUtil.ml @@ -35,8 +35,8 @@ let visit_ast ?(special_k = fun _ -> assert false) k = | Ast.Case (term, indtype, typ, patterns) -> Ast.Case (k term, indtype, aux_opt typ, aux_patterns patterns) | Ast.Cast (t1, t2) -> Ast.Cast (k t1, k t2) - | Ast.LetIn (var, t1, t2) -> - Ast.LetIn (aux_capture_variable var, k t1, k t2) + | Ast.LetIn (var, t1, t3) -> + Ast.LetIn (aux_capture_variable var, k t1, k t3) | Ast.LetRec (kind, definitions, term) -> let definitions = List.map @@ -187,9 +187,9 @@ let meta_names_of_term term = aux term ; aux_opt outty_opt ; List.iter aux_branch patterns - | Ast.LetIn (_, t1, t2) -> + | Ast.LetIn (_, t1, t3) -> aux t1 ; - aux t2 + aux t3 | Ast.LetRec (_, definitions, body) -> List.iter aux_definition definitions ; aux body diff --git a/helm/software/components/acic_content/content.ml b/helm/software/components/acic_content/content.ml index c8b22f497..1e4cc88af 100644 --- a/helm/software/components/acic_content/content.ml +++ b/helm/software/components/acic_content/content.ml @@ -58,7 +58,8 @@ type 'term definition = { def_name : string option; def_id : id ; def_aref : string ; - def_term : 'term + def_term : 'term ; + def_type : 'term } ;; diff --git a/helm/software/components/acic_content/content.mli b/helm/software/components/acic_content/content.mli index 546000330..229d30749 100644 --- a/helm/software/components/acic_content/content.mli +++ b/helm/software/components/acic_content/content.mli @@ -47,7 +47,8 @@ type 'term definition = { def_name : string option; def_id : id ; def_aref : string ; - def_term : 'term + def_term : 'term ; + def_type : 'term } ;; diff --git a/helm/software/components/acic_content/content2cic.ml b/helm/software/components/acic_content/content2cic.ml index dcec61d84..33c5921fb 100644 --- a/helm/software/components/acic_content/content2cic.ml +++ b/helm/software/components/acic_content/content2cic.ml @@ -70,17 +70,22 @@ let proof2cic deannotate p = | None -> C.Lambda (C.Anonymous, deannotate h.Con.dec_type, target)) | `Proof p -> + let ty = + match p.Con.proof_conclude.Con.conclude_conclusion with + None -> (*Cic.Implicit None*) assert false + | Some ty -> deannotate ty + in (match p.Con.proof_name with Some s -> - C.LetIn (C.Name s, proof2cic premise_env p, target) + C.LetIn (C.Name s, proof2cic premise_env p, ty , target) | None -> - C.LetIn (C.Anonymous, proof2cic premise_env p, target)) + C.LetIn (C.Anonymous, proof2cic premise_env p, ty, target)) | `Definition d -> (match d.Con.def_name with Some s -> - C.LetIn (C.Name s, proof2cic premise_env p, target) + C.LetIn (C.Name s, proof2cic premise_env p, deannotate d.Con.def_type, target) | None -> - C.LetIn (C.Anonymous, proof2cic premise_env p, target)) + C.LetIn (C.Anonymous, proof2cic premise_env p, deannotate d.Con.def_type, target)) | `Joint {Con.joint_kind = kind; Con.joint_defs = defs} -> (match target with C.Rel n -> @@ -247,14 +252,14 @@ let cobj2obj deannotate (id,params,metasenv,obj) = | _ -> assert false) | Some (`Definition d) -> (match d with - {K.def_name = Some n ; K.def_term = t} -> - Some (Cic.Name n, Cic.Def ((deannotate t),None)) + {K.def_name = Some n ; K.def_term = t ; K.def_type = ty} -> + Some (Cic.Name n, Cic.Def (deannotate t,deannotate ty)) | _ -> assert false) | Some (`Proof d) -> (match d with {K.proof_name = Some n } -> Some (Cic.Name n, - Cic.Def ((proof2cic deannotate d),None)) + Cic.Def ((proof2cic deannotate d),assert false)) | _ -> assert false) ) canonical_context in diff --git a/helm/software/components/acic_content/termAcicContent.ml b/helm/software/components/acic_content/termAcicContent.ml index f6b1b68aa..f3806beea 100644 --- a/helm/software/components/acic_content/termAcicContent.ml +++ b/helm/software/components/acic_content/termAcicContent.ml @@ -118,8 +118,8 @@ let ast_of_acic0 ~output_type term_info acic k = | Cic.ALambda (id,n,s,t) -> idref id (Ast.Binder (`Lambda, (CicNotationUtil.name_of_cic_name n, Some (k s)), k t)) - | Cic.ALetIn (id,n,s,t) -> - idref id (Ast.LetIn ((CicNotationUtil.name_of_cic_name n, None), + | Cic.ALetIn (id,n,s,ty,t) -> + idref id (Ast.LetIn ((CicNotationUtil.name_of_cic_name n, Some (k ty)), k s, k t)) | Cic.AAppl (aid,(Cic.AConst _ as he::tl as args)) | Cic.AAppl (aid,(Cic.AMutInd _ as he::tl as args)) diff --git a/helm/software/components/acic_procedural/acic2Procedural.ml b/helm/software/components/acic_procedural/acic2Procedural.ml index b4f6053c0..18b4f064f 100644 --- a/helm/software/components/acic_procedural/acic2Procedural.ml +++ b/helm/software/components/acic_procedural/acic2Procedural.ml @@ -300,7 +300,8 @@ and proc_letin st what name v t = in st, C.Decl (H.cic ity), rqv | None -> - st, C.Def (H.cic v, None), [T.LetIn (intro, v, dtext)] + (*CSC: here we need the type of v *) + st, C.Def (H.cic v, assert false), [T.LetIn (intro, v, dtext)] in let entry = Some (name, hyp) in let qt = proc_proof (next (add st entry intro)) t in @@ -385,7 +386,7 @@ and proc_proof st t = in match t with | C.ALambda (_, name, w, t) -> proc_lambda st name w t - | C.ALetIn (_, name, v, t) as what -> proc_letin (f st) what name v t + | C.ALetIn (_, name, v, ty, t) as what -> assert false (*proc_letin (f st) what name v t*) | C.ARel _ as what -> proc_rel (f st) what | C.AMutConstruct _ as what -> proc_mutconstruct (f st) what | C.AAppl (_, hd :: tl) as what -> proc_appl (f st) what hd tl diff --git a/helm/software/components/acic_procedural/proceduralConversion.ml b/helm/software/components/acic_procedural/proceduralConversion.ml index 376313ac8..b3a247b02 100644 --- a/helm/software/components/acic_procedural/proceduralConversion.ml +++ b/helm/software/components/acic_procedural/proceduralConversion.ml @@ -72,7 +72,7 @@ let lift k n = | C.AMutCase (id, sp, i, outty, t, pl) -> C.AMutCase (id, sp, i, lift_term k outty, lift_term k t, List.map (lift_term k) pl) | C.AProd (id, n, s, t) -> C.AProd (id, n, lift_term k s, lift_term (succ k) t) | C.ALambda (id, n, s, t) -> C.ALambda (id, n, lift_term k s, lift_term (succ k) t) - | C.ALetIn (id, n, s, t) -> C.ALetIn (id, n, lift_term k s, lift_term (succ k) t) + | C.ALetIn (id, n, ty, s, t) -> C.ALetIn (id, n, lift_term k s, lift_term k ty, lift_term (succ k) t) | C.AFix (id, i, fl) -> C.AFix (id, i, List.map (lift_fix (List.length fl) k) fl) | C.ACoFix (id, i, fl) -> C.ACoFix (id, i, List.map (lift_cofix (List.length fl) k) fl) in @@ -87,9 +87,9 @@ let lift k n = | Invalid_argument _ -> assert false in let mk_decl n v = Some (n, C.Decl v) in - let mk_def n v = Some (n, C.Def (v, None)) in - let mk_fix (name, _, _, bo) = mk_def (C.Name name) bo in - let mk_cofix (name, _, bo) = mk_def (C.Name name) bo in + let mk_def n v ty = Some (n, C.Def (v, ty)) in + let mk_fix (name, _, ty, bo) = mk_def (C.Name name) bo ty in + let mk_cofix (name, ty, bo) = mk_def (C.Name name) bo ty in let rec ann_xns c (uri, t) = uri, ann_term c t and ann_ms c = function | None -> None @@ -112,7 +112,7 @@ let lift k n = | C.MutCase (sp, i, outty, t, pl) -> C.AMutCase (id, sp, i, ann_term c outty, ann_term c t, List.map (ann_term c) pl) | C.Prod (n, s, t) -> C.AProd (id, n, ann_term c s, ann_term (mk_decl n s :: c) t) | C.Lambda (n, s, t) -> C.ALambda (id, n, ann_term c s, ann_term (mk_decl n s :: c) t) - | C.LetIn (n, s, t) -> C.ALetIn (id, n, ann_term c s, ann_term (mk_def n s :: c) t) + | C.LetIn (n, s, ty, t) -> C.ALetIn (id, n, ann_term c s, ann_term c ty, ann_term (mk_def n s ty :: c) t) | C.Fix (i, fl) -> C.AFix (id, i, List.map (ann_fix (List.rev_map mk_fix fl) c) fl) | C.CoFix (i, fl) -> C.ACoFix (id, i, List.map (ann_cofix (List.rev_map mk_cofix fl) c) fl) in @@ -175,9 +175,9 @@ let generalize n = | C.ALambda (id, _, s, t) -> let s, t = gen_term k s, gen_term (succ k) t in if is_meta [s; t] then meta id else C.ALambda (id, anon, s, t) - | C.ALetIn (id, _, s, t) -> - let s, t = gen_term k s, gen_term (succ k) t in - if is_meta [s; t] then meta id else C.ALetIn (id, anon, s, t) + | C.ALetIn (id, _, s, ty, t) -> + let s, ty, t = gen_term k s, gen_term k ty, gen_term (succ k) t in + if is_meta [s; t] then meta id else C.ALetIn (id, anon, s, ty, t) | C.AFix (id, i, fl) -> C.AFix (id, i, List.map (gen_fix (List.length fl) k) fl) | C.ACoFix (id, i, fl) -> C.ACoFix (id, i, List.map (gen_cofix (List.length fl) k) fl) in @@ -210,9 +210,9 @@ let get_clears c p xtypes = else hd, names, v in - let p = C.LetIn (n, v, p) in - let it = C.LetIn (n, v, it) in - let et = C.LetIn (n, v, et) in + let p = C.LetIn (n, v, assert false, p) in + let it = C.LetIn (n, v, assert false, it) in + let et = C.LetIn (n, v, assert false, et) in aux (hd :: c) names p it et tl | Some (C.Anonymous as n, C.Decl v) as hd :: tl -> let p = C.Lambda (n, meta, p) in @@ -220,9 +220,9 @@ let get_clears c p xtypes = let et = C.Lambda (n, meta, et) in aux (hd :: c) names p it et tl | Some (C.Anonymous as n, C.Def (v, _)) as hd :: tl -> - let p = C.LetIn (n, meta, p) in - let it = C.LetIn (n, meta, it) in - let et = C.LetIn (n, meta, et) in + let p = C.LetIn (n, meta, assert false, p) in + let it = C.LetIn (n, meta, assert false, it) in + let et = C.LetIn (n, meta, assert false, et) in aux (hd :: c) names p it et tl | None :: tl -> assert false in diff --git a/helm/software/components/acic_procedural/proceduralHelpers.ml b/helm/software/components/acic_procedural/proceduralHelpers.ml index fb95a6d0c..31c7f4e8d 100644 --- a/helm/software/components/acic_procedural/proceduralHelpers.ml +++ b/helm/software/components/acic_procedural/proceduralHelpers.ml @@ -180,11 +180,11 @@ let cic_bc c t = let get_fix_decl (sname, i, w, v) = sname, w in let get_cofix_decl (sname, w, v) = sname, w in let rec bc c = function - | C.LetIn (name, v, t) -> + | C.LetIn (name, v, ty, t) -> let name = mk_fresh_name c name in - let entry = Some (name, C.Def (v, None)) in - let v, t = bc c v, bc (entry :: c) t in - C.LetIn (name, v, t) + let entry = Some (name, C.Def (v, ty)) in + let v, ty, t = bc c v, bc c ty, bc (entry :: c) t in + C.LetIn (name, v, ty, t) | C.Lambda (name, w, t) -> let name = mk_fresh_name c name in let entry = Some (name, C.Decl w) in @@ -222,11 +222,11 @@ let acic_bc c t = let get_fix_decl (id, sname, i, w, v) = sname, cic w in let get_cofix_decl (id, sname, w, v) = sname, cic w in let rec bc c = function - | C.ALetIn (id, name, v, t) -> + | C.ALetIn (id, name, v, ty, t) -> let name = mk_fresh_name c name in - let entry = Some (name, C.Def (cic v, None)) in - let v, t = bc c v, bc (entry :: c) t in - C.ALetIn (id, name, v, t) + let entry = Some (name, C.Def (cic v, cic ty)) in + let v, ty, t = bc c v, bc c ty, bc (entry :: c) t in + C.ALetIn (id, name, v, ty, t) | C.ALambda (id, name, w, t) -> let name = mk_fresh_name c name in let entry = Some (name, C.Decl (cic w)) in diff --git a/helm/software/components/acic_procedural/proceduralOptimizer.ml b/helm/software/components/acic_procedural/proceduralOptimizer.ml index 1953ae7f1..88ad74a66 100644 --- a/helm/software/components/acic_procedural/proceduralOptimizer.ml +++ b/helm/software/components/acic_procedural/proceduralOptimizer.ml @@ -40,7 +40,8 @@ let defined_premise = "DEFINED" let define v = let name = C.Name defined_premise in - C.LetIn (name, v, C.Rel 1) + (*CSC: here we need the type of v *) + C.LetIn (name, v, assert false, C.Rel 1) let clear_absts m = let rec aux k n = function @@ -62,21 +63,25 @@ let rec add_abst k = function let rec opt1_letin g es c name v t = let name = H.mk_fresh_name c name in - let entry = Some (name, C.Def (v, None)) in + (*CSC: here we need the type of v *) + let entry = Some (name, C.Def (v, assert false)) in let g t = if DTI.does_not_occur 1 t then begin let x = S.lift (-1) t in HLog.warn "Optimizer: remove 1"; opt1_proof g true c x end else let g = function - | C.LetIn (nname, vv, tt) when H.is_proof c v -> - let x = C.LetIn (nname, vv, C.LetIn (name, tt, S.lift_from 2 1 t)) in + | C.LetIn (nname, vv, tyty, tt) when H.is_proof c v -> + (*CSC: here we need the type of v *) + let x = C.LetIn (nname, vv, tyty, + C.LetIn (name, tt, assert false, S.lift_from 2 1 t)) in HLog.warn "Optimizer: swap 1"; opt1_proof g true c x | v when H.is_proof c v && H.is_atomic v -> let x = S.subst v t in HLog.warn "Optimizer: remove 5"; opt1_proof g true c x | v -> - g (C.LetIn (name, v, t)) + (*CSC: here we need the type of v *) + g (C.LetIn (name, v, assert false, t)) in if es then opt1_term g es c v else g v in @@ -91,13 +96,14 @@ and opt1_lambda g es c name w t = and opt1_appl g es c t vs = let g vs = let g = function - | C.LetIn (mame, vv, tt) -> + | C.LetIn (mame, vv, tyty, tt) -> let vs = List.map (S.lift 1) vs in - let x = C.LetIn (mame, vv, C.Appl (tt :: vs)) in + let x = C.LetIn (mame, vv, tyty, C.Appl (tt :: vs)) in HLog.warn "Optimizer: swap 2"; opt1_proof g true c x | C.Lambda (name, ww, tt) -> let v, vs = List.hd vs, List.tl vs in - let x = C.Appl (C.LetIn (name, v, tt) :: vs) in + (*CSC: here we need the type of v *) + let x = C.Appl (C.LetIn (name, v, assert false, tt) :: vs) in HLog.warn "Optimizer: remove 2"; opt1_proof g true c x | C.Appl vvs -> let x = C.Appl (vvs @ vs) in @@ -132,12 +138,13 @@ and opt1_appl g es c t vs = aux false [] (vs, classes) *) in let rec aux h prev = function - | C.LetIn (name, vv, tt) :: vs -> + | C.LetIn (name, vv, tyty, tt) :: vs -> let t = S.lift 1 t in let prev = List.map (S.lift 1) prev in let vs = List.map (S.lift 1) vs in let y = C.Appl (t :: List.rev prev @ tt :: vs) in - let x = C.LetIn (name, vv, y) in + (*CSC: here we need the type of vv *) + let x = C.LetIn (name, vv, assert false, y) in HLog.warn "Optimizer: swap 3"; opt1_proof g true c x | v :: vs -> aux h (v :: prev) vs | [] -> h () @@ -184,7 +191,8 @@ and opt1_cast g es c t w = and opt1_other g es c t = g t and opt1_proof g es c = function - | C.LetIn (name, v, t) -> opt1_letin g es c name v t + (*CSC: what to do now that we have also ty? *) + | C.LetIn (name, v, ty, t) -> assert false (*opt1_letin g es c name v t*) | C.Lambda (name, w, t) -> opt1_lambda g es c name w t | C.Appl (t :: v :: vs) -> opt1_appl g es c t (v :: vs) | C.Appl [t] -> opt1_proof g es c t @@ -217,9 +225,11 @@ let eta_expand g tys t = g (absts t) let rec opt2_letin g c name v t = - let entry = Some (name, C.Def (v, None)) in + (*CSC: here we need the type of v *) + let entry = Some (name, C.Def (v, assert false)) in let g t = - let g v = g (C.LetIn (name, v, t)) in + (*CSC: here we need the type of v *) + let g v = g (C.LetIn (name, v, assert false, t)) in opt2_term g c v in opt2_proof g (entry :: c) t @@ -251,7 +261,8 @@ and opt2_other g c t = end else g t and opt2_proof g c = function - | C.LetIn (name, v, t) -> opt2_letin g c name v t + (*CSC: what to do now that we have also ty? *) + | C.LetIn (name, v, ty, t) -> assert false (*opt2_letin g c name v t*) | C.Lambda (name, w, t) -> opt2_lambda g c name w t | C.Appl (t :: vs) -> opt2_appl g c t vs | t -> opt2_other g c t diff --git a/helm/software/components/cic/cic.ml b/helm/software/components/cic/cic.ml index 1b02df3f1..5dd8455ea 100644 --- a/helm/software/components/cic/cic.ml +++ b/helm/software/components/cic/cic.ml @@ -95,7 +95,7 @@ type term = | Cast of term * term (* value, type *) | Prod of name * term * term (* binder, source, target *) | Lambda of name * term * term (* binder, source, target *) - | LetIn of name * term * term (* binder, term, target *) + | LetIn of name * term * term * term (* binder, term, type, target *) | Appl of term list (* arguments *) | Const of UriManager.uri * (* uri, *) term explicit_named_substitution (* explicit named subst. *) @@ -159,7 +159,7 @@ and annterm = | ACast of id * annterm * annterm (* value, type *) | AProd of id * name * annterm * annterm (* binder, source, target *) | ALambda of id * name * annterm * annterm (* binder, source, target *) - | ALetIn of id * name * annterm * annterm (* binder, term, target *) + | ALetIn of id * name * annterm * annterm * annterm (* binder, term, type, target *) | AAppl of id * annterm list (* arguments *) | AConst of id * UriManager.uri * (* uri, *) annterm explicit_named_substitution (* explicit named subst. *) @@ -205,7 +205,7 @@ and annotation = and context_entry = (* A declaration or definition *) Decl of term - | Def of term * term option (* body, type (if known) *) + | Def of term * term (* body, type *) and hypothesis = (name * context_entry) option (* None means no more accessible *) @@ -214,7 +214,7 @@ and context = hypothesis list and anncontext_entry = (* A declaration or definition *) ADecl of annterm - | ADef of annterm + | ADef of annterm * annterm and annhypothesis = id * (name * anncontext_entry) option (* None means no more accessible *) diff --git a/helm/software/components/cic/cicInspect.ml b/helm/software/components/cic/cicInspect.ml index a1e94e247..cc911df84 100644 --- a/helm/software/components/cic/cicInspect.ml +++ b/helm/software/components/cic/cicInspect.ml @@ -56,9 +56,10 @@ let get_rels_from_premise h t = in List.fold_left map g ss | C.Cast (t1, t2) -> aux d (aux d g t2) t1 - | C.LetIn (_, t1, t2) | C.Lambda (_, t1, t2) | C.Prod (_, t1, t2) -> aux d (aux (succ d) g t2) t1 + | C.LetIn (_, t1, ty, t2) -> + aux d (aux d (aux (succ d) g t2) ty) t1 | C.MutCase (_, _, t1, t2, ss) -> aux d (aux d (List.fold_left (aux d) g ss) t2) t1 | C.Fix (_, ss) -> @@ -95,9 +96,9 @@ let get_mutinds_of_uri u t = in List.fold_left map g ss | C.Cast (t1, t2) -> aux (aux g t2) t1 - | C.LetIn (_, t1, t2) | C.Lambda (_, t1, t2) - | C.Prod (_, t1, t2) -> aux (aux g t2) t1 + | C.Prod (_, t1, t2) -> aux (aux g t2) t1 + | C.LetIn (_, t1, ty, t2) -> aux (aux (aux g t2) ty) t1 | C.MutCase (_, _, t1, t2, ss) -> aux (aux (List.fold_left aux g ss) t2) t1 | C.Fix (_, ss) -> @@ -128,9 +129,9 @@ let rec aux n = function in List.fold_left map (succ n) ss | C.Cast (t1, t2) - | C.LetIn (_, t1, t2) | C.Lambda (_, t1, t2) - | C.Prod (_, t1, t2) -> aux (aux (succ n) t2) t1 + | C.Prod (_, t1, t2) -> aux (aux (succ n) t2) t1 + | C.LetIn (_, t1, ty, t2) -> aux (aux (aux (succ n) t2) ty) t1 | C.MutCase (_, _, t1, t2, ss) -> aux (aux (List.fold_left aux (succ n) ss) t2) t1 | C.Fix (_, ss) -> diff --git a/helm/software/components/cic/cicParser.ml b/helm/software/components/cic/cicParser.ml index 8334ccfb6..3d1d3d1aa 100644 --- a/helm/software/components/cic/cicParser.ml +++ b/helm/software/components/cic/cicParser.ml @@ -60,7 +60,7 @@ type stack_entry = (* id, name, type, body *) | Constructor of string * Cic.annterm (* name, type *) | Decl of Cic.id * Cic.name * Cic.annterm (* id, binder, source *) - | Def of Cic.id * Cic.name * Cic.annterm (* id, binder, source *) + | Def of Cic.id * Cic.name * Cic.annterm * Cic.annterm (* id, binder, source, type *) | Fix_fun of Cic.id * string * int * Cic.annterm * Cic.annterm (* id, name, ind. index, type, body *) | Inductive_type of string * string * bool * Cic.annterm * @@ -97,7 +97,7 @@ let string_of_stack ctxt = | Constructor (name, _) -> "Constructor " ^ name | Cofix_fun (id, _, _, _) -> sprintf "Cofix_fun (id=%s)" id | Decl (id, _, _) -> sprintf "Decl (id=%s)" id - | Def (id, _, _) -> sprintf "Def (id=%s)" id + | Def (id, _, _, _) -> sprintf "Def (id=%s)" id | Fix_fun (id, _, _, _, _) -> sprintf "Fix_fun (id=%s)" id | Inductive_type (id, name, _, _, _) -> sprintf "Inductive_type %s (id=%s)" name id @@ -406,14 +406,15 @@ let end_element ctxt tag = | ["id", id; "type", _] -> Decl (id, Cic.Anonymous, source) | _ -> attribute_error ()) | "def" -> (* same as "decl" above *) + let ty = pop_cic ctxt in let source = pop_cic ctxt in push ctxt (match pop_tag_attrs ctxt with | ["binder", binder; "id", id] | ["binder", binder; "id", id; "sort", _] -> - Def (id, Cic.Name binder, source) + Def (id, Cic.Name binder, source, ty) | ["id", id] - | ["id", id; "sort", _] -> Def (id, Cic.Anonymous, source) + | ["id", id; "sort", _] -> Def (id, Cic.Anonymous, source, ty) | _ -> attribute_error ()) | "arity" (* transparent elements (i.e. which contain a CIC) *) | "body" @@ -467,8 +468,8 @@ let end_element ctxt tag = | "LETIN" -> let target = pop_cic ctxt in let rec add_def target = function - | Def (id, binder, source) :: tl -> - add_def (Cic.ALetIn (id, binder, source, target)) tl + | Def (id, binder, source, ty) :: tl -> + add_def (Cic.ALetIn (id, binder, source, ty, target)) tl | tl -> ctxt.stack <- tl; target diff --git a/helm/software/components/cic/cicUtil.ml b/helm/software/components/cic/cicUtil.ml index dd1652196..75b7fd2cc 100644 --- a/helm/software/components/cic/cicUtil.ml +++ b/helm/software/components/cic/cicUtil.ml @@ -79,7 +79,8 @@ let is_closed = | C.Cast (te,ty) -> is_closed k te && is_closed k ty | C.Prod (name,so,dest) -> is_closed k so && is_closed (k+1) dest | C.Lambda (_,so,dest) -> is_closed k so && is_closed (k+1) dest - | C.LetIn (_,so,dest) -> is_closed k so && is_closed (k+1) dest + | C.LetIn (_,so,ty,dest) -> + is_closed k so && is_closed k ty && is_closed (k+1) dest | C.Appl l -> List.fold_right (fun x i -> i && is_closed k x) l true | C.Var (_,exp_named_subst) @@ -116,7 +117,10 @@ let rec is_meta_closed = | C.Cast (te,ty) -> is_meta_closed te && is_meta_closed ty | C.Prod (name,so,dest) -> is_meta_closed so && is_meta_closed dest | C.Lambda (_,so,dest) -> is_meta_closed so && is_meta_closed dest - | C.LetIn (_,so,dest) -> is_meta_closed so && is_meta_closed dest + | C.LetIn (_,so,ty,dest) -> + is_meta_closed so && + is_meta_closed ty && + is_meta_closed dest | C.Appl l -> not (List.exists (fun x -> not (is_meta_closed x)) l) | C.Var (_,exp_named_subst) @@ -250,7 +254,7 @@ let id_of_annterm = | C.ACast (id,_,_) | C.AProd (id,_,_,_) | C.ALambda (id,_,_,_) - | C.ALetIn (id,_,_,_) + | C.ALetIn (id,_,_,_,_) | C.AAppl (id,_) | C.AConst (id,_,_) | C.AMutInd (id,_,_,_) @@ -290,7 +294,8 @@ let rec rehash_term = | C.Cast (te,ty) -> C.Cast (rehash_term te, rehash_term ty) | C.Prod (n,s,t) -> C.Prod (n, rehash_term s, rehash_term t) | C.Lambda (n,s,t) -> C.Lambda (n, rehash_term s, rehash_term t) - | C.LetIn (n,s,t) -> C.LetIn (n, rehash_term s, rehash_term t) + | C.LetIn (n,s,ty,t) -> + C.LetIn (n, rehash_term s, rehash_term ty, rehash_term t) | C.Appl l -> C.Appl (List.map rehash_term l) | C.Const (uri,exp_named_subst) -> let uri' = recons uri in @@ -355,12 +360,7 @@ let rehash_obj = | Some (name,C.Decl t) -> Some (name,C.Decl (rehash_term t)) | Some (name,C.Def (bo,ty)) -> - let ty' = - match ty with - None -> None - | Some ty'' -> Some (rehash_term ty'') - in - Some (name,C.Def (rehash_term bo, ty'))) hyps, + Some (name,C.Def (rehash_term bo, rehash_term ty))) hyps, rehash_term ty)) conjs in @@ -400,8 +400,9 @@ let rec metas_of_term = function List.flatten (List.map (fun (u, t) -> metas_of_term t) ens) | C.Cast (s, t) | C.Prod (_, s, t) - | C.Lambda (_, s, t) - | C.LetIn (_, s, t) -> (metas_of_term s) @ (metas_of_term t) + | C.Lambda (_, s, t) -> (metas_of_term s) @ (metas_of_term t) + | C.LetIn (_, s, ty, t) -> + (metas_of_term s) @ (metas_of_term ty) @ (metas_of_term t) | C.Appl l -> List.flatten (List.map metas_of_term l) | C.MutCase (uri, i, s, t, l) -> (metas_of_term s) @ (metas_of_term t) @ @@ -435,8 +436,10 @@ let rec metas_of_term_set = function S.empty ens | C.Cast (s, t) | C.Prod (_, s, t) - | C.Lambda (_, s, t) - | C.LetIn (_, s, t) -> S.union (metas_of_term_set s) (metas_of_term_set t) + | C.Lambda (_, s, t) -> S.union (metas_of_term_set s) (metas_of_term_set t) + | C.LetIn (_, s, ty, t) -> + S.union (metas_of_term_set s) + (S.union (metas_of_term_set ty) (metas_of_term_set t)) | C.Appl l -> List.fold_left (fun s t -> S.union s (metas_of_term_set t)) @@ -482,8 +485,8 @@ let alpha_equivalence = aux s s' && aux t t' | C.Lambda (_,s,t), C.Lambda (_,s',t') -> aux s s' && aux t t' - | C.LetIn (_,s,t), C.LetIn(_,s',t') -> - aux s s' && aux t t' + | C.LetIn (_,s,ty,t), C.LetIn(_,s',ty',t') -> + aux s s' && aux ty ty' && aux t t' | C.Appl l, C.Appl l' when List.length l = List.length l' -> (try List.fold_left2 @@ -564,10 +567,11 @@ let is_sober t = | C.MutConstruct (_, _, _, xnss) | C.MutInd (_, _, xnss) -> sober_xnss g xnss | C.Meta (_, xss) -> sober_xss g xss - | C.LetIn (_, v, t) | C.Lambda (_, v, t) | C.Prod (_, v, t) | C.Cast (t, v) -> sober_term (sober_term g t) v + | C.LetIn (_, v, ty, t) -> sober_term + (sober_term (sober_term g t) ty) v | C.Appl [] | C.Appl [_] -> fun b -> false | C.Appl ts -> sober_terms g ts diff --git a/helm/software/components/cic/deannotate.ml b/helm/software/components/cic/deannotate.ml index b7c7d1113..f1dfbffed 100644 --- a/helm/software/components/cic/deannotate.ml +++ b/helm/software/components/cic/deannotate.ml @@ -51,8 +51,8 @@ let rec deannotate_term = C.Prod (name, deannotate_term so, deannotate_term ta) | C.ALambda (_,name,so,ta) -> C.Lambda (name, deannotate_term so, deannotate_term ta) - | C.ALetIn (_,name,so,ta) -> - C.LetIn (name, deannotate_term so, deannotate_term ta) + | C.ALetIn (_,name,so,ty,ta) -> + C.LetIn (name, deannotate_term so, deannotate_term ty, deannotate_term ta) | C.AAppl (_,l) -> C.Appl (List.map deannotate_term l) | C.AConst (_,uri,exp_named_subst) -> let deann_exp_named_subst = @@ -97,7 +97,8 @@ let deannotate_conjectures = let context = List.map (function - | _,Some (n,(C.ADef at)) -> Some(n,(C.Def((deannotate_term at),None))) + | _,Some (n,(C.ADef (ate,aty))) -> + Some(n,(C.Def(deannotate_term ate,deannotate_term aty))) | _,Some (n,(C.ADecl at)) -> Some (n,(C.Decl (deannotate_term at))) | _,None -> None) acontext diff --git a/helm/software/components/cic/unshare.ml b/helm/software/components/cic/unshare.ml index e198bcd49..e4d2cc74a 100644 --- a/helm/software/components/cic/unshare.ml +++ b/helm/software/components/cic/unshare.ml @@ -48,7 +48,8 @@ let rec unshare = | C.Cast (te,ty) -> C.Cast (unshare te, unshare ty) | C.Prod (n,s,t) -> C.Prod (n, unshare s, unshare t) | C.Lambda (n,s,t) -> C.Lambda (n, unshare s, unshare t) - | C.LetIn (n,s,t) -> C.LetIn (n, unshare s, unshare t) + | C.LetIn (n,s,ty,t) -> + C.LetIn (n, unshare s, unshare ty, unshare t) | C.Appl l -> C.Appl (List.map unshare l) | C.Const (uri,exp_named_subst) -> let exp_named_subst' = diff --git a/helm/software/components/cic_acic/cic2Xml.ml b/helm/software/components/cic_acic/cic2Xml.ml index eb3b93408..0708a839f 100644 --- a/helm/software/components/cic_acic/cic2Xml.ml +++ b/helm/software/components/cic_acic/cic2Xml.ml @@ -137,21 +137,21 @@ let print_term ?ids_to_inner_sorts = ) [< >] lambdas ; X.xml_nempty "target" [] (aux t) >] - | C.ALetIn (xid,C.Anonymous,s,t) -> + | C.ALetIn (xid,C.Anonymous,s,ty,t) -> assert false - | C.ALetIn (last_id,C.Name _,_,_) as letins -> + | C.ALetIn (last_id,C.Name _,_,_,_) as letins -> let rec eat_letins = function - C.ALetIn (id,n,s,t) -> + C.ALetIn (id,n,s,ty,t) -> let letins,t' = eat_letins t in - (id,n,s)::letins,t' + (id,n,s,ty)::letins,t' | t -> [],t in let letins,t = eat_letins letins in let sort = find_sort "sort" last_id in X.xml_nempty "LETIN" sort [< List.fold_left - (fun i (id,binder,s) -> + (fun i (id,binder,s,ty) -> let sort = find_sort "sort" id in let attrs = sort @ ((None,"id",id):: @@ -159,7 +159,7 @@ let print_term ?ids_to_inner_sorts = C.Anonymous -> [] | C.Name b -> [None,"binder",b]) in - [< i ; X.xml_nempty "def" attrs (aux s) >] + [< i ; X.xml_nempty "def" attrs [< aux s ; aux ty >] >] ) [< >] letins ; X.xml_nempty "target" [] (aux t) >] @@ -345,7 +345,7 @@ let print_object uri [None,"id",hid;None,"name",n'] | C.Anonymous -> [None,"id",hid]) (print_term ?ids_to_inner_sorts t) - | Some (n,C.ADef t) -> + | Some (n,C.ADef (t,_)) -> X.xml_nempty "Def" (match n with C.Name n' -> diff --git a/helm/software/components/cic_acic/cic2acic.ml b/helm/software/components/cic_acic/cic2acic.ml index bb00476b9..c5bbfff78 100644 --- a/helm/software/components/cic_acic/cic2acic.ml +++ b/helm/software/components/cic_acic/cic2acic.ml @@ -300,20 +300,13 @@ let acic_of_cic_context' ~computeinnertypes:global_computeinnertypes C.ALambda (fresh_id'',n, aux' context idrefs s, aux' ((Some (n, C.Decl s)::context)) (fresh_id''::idrefs) t) - | C.LetIn (n,s,t) -> - let s_ty = - try - (cic_CicHash_find terms_to_types s).D.synthesized - with - Not_found -> - cicReduction_whd context (xxx_type_of_aux' metasenv context s); - in + | C.LetIn (n,s,ty,t) -> xxx_add ids_to_inner_sorts fresh_id'' innersort ; if innersort = `Prop then add_inner_type fresh_id'' ; C.ALetIn - (fresh_id'', n, aux' context idrefs s, - aux' ((Some (n, C.Def(s,Some s_ty)))::context) (fresh_id''::idrefs) t) + (fresh_id'', n, aux' context idrefs s, aux' context idrefs ty, + aux' ((Some (n, C.Def(s,ty)))::context) (fresh_id''::idrefs) t) | C.Appl l -> xxx_add ids_to_inner_sorts fresh_id'' innersort ; if innersort = `Prop then @@ -429,12 +422,21 @@ let aconjecture_of_conjecture seed ids_to_terms ids_to_father_ids Hashtbl.add ids_to_hypotheses hid binding ; incr hypotheses_seed ; match binding with - Some (n,Cic.Def (t,_)) -> - let acic = acic_of_cic_context ~computeinnertypes context idrefs t None in - Hashtbl.replace ids_to_father_ids (CicUtil.id_of_annterm acic) - (Some hid); - (binding::context), - ((hid,Some (n,Cic.ADef acic))::acontext),(hid::idrefs) + Some (n,Cic.Def (t,ty)) -> + let acic = + acic_of_cic_context ~computeinnertypes context idrefs t + None in + let acic2 = + acic_of_cic_context ~computeinnertypes context idrefs ty + None + in + Hashtbl.replace ids_to_father_ids (CicUtil.id_of_annterm acic) + (Some hid); + Hashtbl.replace ids_to_father_ids + (CicUtil.id_of_annterm acic2) (Some hid); + (binding::context), + ((hid,Some (n,Cic.ADef (acic,acic2)))::acontext), + (hid::idrefs) | Some (n,Cic.Decl t) -> let acic = acic_of_cic_context ~computeinnertypes context idrefs t None in Hashtbl.replace ids_to_father_ids (CicUtil.id_of_annterm acic) @@ -469,10 +471,8 @@ let asequent_of_sequent (metasenv:Cic.metasenv) (sequent:Cic.conjecture) = None -> None | Some (n, Cic.Decl t)-> Some (n, Cic.Decl (Unshare.unshare t)) - | Some (n, Cic.Def (t,None)) -> - Some (n, Cic.Def ((Unshare.unshare t),None)) - | Some (n,Cic.Def (bo,Some ty)) -> - Some (n, Cic.Def (Unshare.unshare bo,Some (Unshare.unshare ty))) + | Some (n,Cic.Def (bo,ty)) -> + Some (n, Cic.Def (Unshare.unshare bo,Unshare.unshare ty)) in d::canonical_context' ) canonical_context [] @@ -549,10 +549,11 @@ let acic_object_of_cic_object ?(eta_fix=false) obj = None -> None | Some (n, C.Decl t)-> Some (n, C.Decl (eta_fix_and_unshare conjectures canonical_context' t)) - | Some (n, C.Def (t,None)) -> + | Some (n, C.Def (t,ty)) -> Some (n, - C.Def ((eta_fix_and_unshare conjectures canonical_context' t),None)) - | Some (_,C.Def (_,Some _)) -> assert false + C.Def + (eta_fix_and_unshare conjectures canonical_context' t, + eta_fix_and_unshare conjectures canonical_context' ty)) in d::canonical_context' ) canonical_context [] @@ -667,10 +668,10 @@ let plain_acic_term_of_cic_term = C.ALambda (fresh_id,n, aux context s, aux ((fresh_id, Some (n, C.Decl s))::context) t) - | C.LetIn (n,s,t) -> + | C.LetIn (n,s,ty,t) -> C.ALetIn - (fresh_id, n, aux context s, - aux ((fresh_id, Some (n, C.Def(s,None)))::context) t) + (fresh_id, n, aux context s, aux context ty, + aux ((fresh_id, Some (n, C.Def(s,ty)))::context) t) | C.Appl l -> C.AAppl (fresh_id, List.map (aux context) l) | C.Const (uri,exp_named_subst) -> diff --git a/helm/software/components/cic_acic/doubleTypeInference.ml b/helm/software/components/cic_acic/doubleTypeInference.ml index 905d1e6bc..4910275ea 100644 --- a/helm/software/components/cic_acic/doubleTypeInference.ml +++ b/helm/software/components/cic_acic/doubleTypeInference.ml @@ -64,9 +64,10 @@ let rec does_not_occur n = | C.Lambda (name,so,dest) -> does_not_occur n so && does_not_occur (n + 1) dest - | C.LetIn (name,so,dest) -> + | C.LetIn (name,so,ty,dest) -> does_not_occur n so && - does_not_occur (n + 1) dest + does_not_occur n ty && + does_not_occur (n + 1) dest | C.Appl l -> List.fold_right (fun x i -> i && does_not_occur n x) l true | C.Var (_,exp_named_subst) @@ -119,8 +120,8 @@ let rec beta_reduce = C.Prod (n, beta_reduce s, beta_reduce t) | C.Lambda (n,s,t) -> C.Lambda (n, beta_reduce s, beta_reduce t) - | C.LetIn (n,s,t) -> - C.LetIn (n, beta_reduce s, beta_reduce t) + | C.LetIn (n,s,ty,t) -> + C.LetIn (n, beta_reduce s, beta_reduce ty, beta_reduce t) | C.Appl ((C.Lambda (name,s,t))::he::tl) -> let he' = S.subst he t in if tl = [] then @@ -271,10 +272,8 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty = (try match List.nth context (n - 1) with Some (_,C.Decl t) -> S.lift n t - | Some (_,C.Def (_,Some ty)) -> S.lift n ty - | Some (_,C.Def (bo,None)) -> - type_of_aux context (S.lift n bo) expectedty - | None -> raise RelToHiddenHypothesis + | Some (_,C.Def (_,ty)) -> S.lift n ty + | None -> raise RelToHiddenHypothesis with _ -> raise (NotWellTyped "Not a close term") ) @@ -290,11 +289,12 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty = [] -> [] | (Some (n,C.Decl t))::tl -> (Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl) - | (Some (n,C.Def (t,None)))::tl -> - (Some (n,C.Def ((S.subst_meta l (S.lift i t)),None))):: - (aux (i+1) tl) + | (Some (n,C.Def (t,ty)))::tl -> + (Some (n, + C.Def + ((S.subst_meta l (S.lift i t)),S.subst_meta l (S.lift i t)))):: + (aux (i+1) tl) | None::tl -> None::(aux (i+1) tl) - | (Some (_,C.Def (_,Some _)))::_ -> assert false in aux 1 canonical_context in @@ -356,21 +356,22 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty = in (* Checks suppressed *) C.Prod (n,s,type2) - | C.LetIn (n,s,t) -> + | C.LetIn (n,s,ty,t) -> (*CSC: What are the right expected types for the source and *) (*CSC: target of a LetIn? None used. *) (* Let's visit all the subterms that will not be visited later *) - let ty = type_of_aux context s None in + let _ = type_of_aux context ty None in + let _ = type_of_aux context s (Some ty) in let t_typ = (* Checks suppressed *) - type_of_aux ((Some (n,(C.Def (s,Some ty))))::context) t None + type_of_aux ((Some (n,(C.Def (s,ty))))::context) t None 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 *) CicSubstitution.subst (C.Implicit None) t_typ else - C.LetIn (n,s,t_typ) + C.LetIn (n,s,ty,t_typ) | C.Appl (he::tl) when List.length tl > 0 -> (* let expected_hetype = @@ -590,7 +591,7 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty = in let rec check uris_and_types subst = match uris_and_types,subst with - _,[] -> [] + _,[] -> () | (uri,ty)::tytl,(uri',t)::substtl when uri = uri' -> ignore (type_of_aux context t (Some ty)) ; let tytl' = diff --git a/helm/software/components/cic_acic/eta_fixing.ml b/helm/software/components/cic_acic/eta_fixing.ml index 78789179f..90f33d081 100644 --- a/helm/software/components/cic_acic/eta_fixing.ml +++ b/helm/software/components/cic_acic/eta_fixing.ml @@ -84,7 +84,8 @@ let rec fix_lambdas_wrt_type ty te = let t2 = match t' with C.Appl l -> - C.LetIn (C.Name "w",t',C.Appl ((C.Rel 1)::(mk_rels no_sources 1))) + C.LetIn (C.Name "w",t',assert false, + C.Appl ((C.Rel 1)::(mk_rels no_sources 1))) | _ -> C.Appl (t'::(mk_rels no_sources 0)) in List.fold_right (fun source t -> C.Lambda (C.Name "y",CicReduction.whd [] source,t)) sources t2 @@ -145,7 +146,9 @@ let fix_according_to_type ty hd tl = (* prerr_endline ("******* too many args: type=" ^ CicPp.ppterm ty ^ "term=" ^ CicPp.ppterm (C.Appl res)); *) C.LetIn (C.Name "H", - C.Appl res, C.Appl (C.Rel 1::(List.map (S.lift 1) tl)))) + C.Appl res, + assert false, + C.Appl (C.Rel 1::(List.map (S.lift 1) tl)))) else let name,source,target = (match ty with @@ -199,9 +202,10 @@ let eta_fix metasenv context t = | C.Lambda (n,s,t) -> C.Lambda (n, eta_fix' context s, eta_fix' ((Some (n,(C.Decl s)))::context) t) - | C.LetIn (n,s,t) -> + | C.LetIn (n,s,ty,t) -> C.LetIn - (n,eta_fix' context s,eta_fix' ((Some (n,(C.Def (s,None))))::context) t) + (n,eta_fix' context s,eta_fix' context ty, + eta_fix' ((Some (n,(C.Def (s,ty))))::context) t) | C.Appl [] -> assert false | C.Appl (he::tl) -> let tl' = List.map (eta_fix' context) tl in diff --git a/helm/software/components/cic_disambiguation/disambiguate.ml b/helm/software/components/cic_disambiguation/disambiguate.ml index dbdb1530f..d58dc9854 100644 --- a/helm/software/components/cic_disambiguation/disambiguate.ml +++ b/helm/software/components/cic_disambiguation/disambiguate.ml @@ -345,13 +345,13 @@ let interpretate_term ?(create_dummy_ids=false) ~(context: Cic.name list) ~env ~ | CicNotationPt.LetIn ((name, typ), def, body) -> let cic_def = aux ~localize loc context def in let cic_name = CicNotationUtil.cic_name_of_name name in - let cic_def = + let cic_typ = match typ with - | None -> cic_def - | Some t -> Cic.Cast (cic_def, aux ~localize loc context t) + | None -> Cic.Implicit (Some `Type) + | Some t -> aux ~localize loc context t in let cic_body = aux ~localize loc (cic_name :: context) body in - Cic.LetIn (cic_name, cic_def, cic_body) + Cic.LetIn (cic_name, cic_def, cic_typ, cic_body) | CicNotationPt.LetRec (kind, defs, body) -> let context' = List.fold_left @@ -431,9 +431,9 @@ let interpretate_term ?(create_dummy_ids=false) ~(context: Cic.name list) ~env ~ Cic.CoFix (n,coinductiveFuns) in let counter = ref ~-1 in - let build_term funs (var,_,_,_) t = + let build_term funs (var,_,ty,_) t = incr counter; - Cic.LetIn (Cic.Name var, fix_or_cofix !counter, t) + Cic.LetIn (Cic.Name var, fix_or_cofix !counter, ty, t) in (match cic_body with `AvoidLetInNoAppl n -> diff --git a/helm/software/components/cic_exportation/cicExportation.ml b/helm/software/components/cic_exportation/cicExportation.ml index 58e817091..dd3be7572 100644 --- a/helm/software/components/cic_exportation/cicExportation.ml +++ b/helm/software/components/cic_exportation/cicExportation.ml @@ -182,20 +182,14 @@ let rec pp ~in_type t context = | `Type -> "(function " ^ ppname b ^ " -> " ^ pp ~in_type t ((Some (b,Cic.Decl s))::context) ^ ")") - | C.LetIn (b,s,t) -> + | C.LetIn (b,s,ty,t) -> (match analyze_term context s with `Type - | `Proof -> - let ty,_ = - CicTypeChecker.type_of_aux' [] context s CicUniv.oblivion_ugraph - in - pp ~in_type t ((Some (b,Cic.Def (s,Some ty)))::context) + | `Proof -> pp ~in_type t ((Some (b,Cic.Def (s,ty)))::context) | `Term -> - let ty,_ = - CicTypeChecker.type_of_aux' [] context s CicUniv.oblivion_ugraph - in - "(let " ^ ppname b ^ " = " ^ pp ~in_type:false s context ^ " in " ^ - pp ~in_type t ((Some (b,Cic.Def (s,Some ty)))::context) ^ ")") + "(let " ^ ppname b ^ " : " ^ pp ~in_type:true ty context ^ + " = " ^ pp ~in_type:false s context ^ " in " ^ + pp ~in_type t ((Some (b,Cic.Def (s,ty)))::context) ^ ")") | C.Appl (he::tl) when in_type -> let hes = pp ~in_type he context in let stl = String.concat "," (clean_args_for_ty context tl) in @@ -570,14 +564,16 @@ let ppobj current_module_uri obj = pp ~in_type:true ~metasenv:conjectures at name_context ^ " ", context_entry::name_context - | Some (n,C.Def (at,None)) -> + | Some (n,C.Def (at,aty)) -> (separate i) ^ - ppname n ^ ":= " ^ pp ~in_type:false + ppname n ^ ":" ^ + pp ~in_type:true ~metasenv:conjectures + aty name_context ^ + ":= " ^ pp ~in_type:false ~metasenv:conjectures at name_context ^ " ", context_entry::name_context | None -> - (separate i) ^ "_ :? _ ", context_entry::name_context - | _ -> assert false) + (separate i) ^ "_ :? _ ", context_entry::name_context) ) context ("",[]) in conjectures' ^ " |- " ^ "?" ^ (string_of_int n) ^ ": " ^ diff --git a/helm/software/components/cic_proof_checking/cicMiniReduction.ml b/helm/software/components/cic_proof_checking/cicMiniReduction.ml index 5c88713c5..f063c1d9b 100644 --- a/helm/software/components/cic_proof_checking/cicMiniReduction.ml +++ b/helm/software/components/cic_proof_checking/cicMiniReduction.ml @@ -40,7 +40,7 @@ let rec letin_nf = | C.Cast (te,ty) -> C.Cast (letin_nf te, letin_nf ty) | C.Prod (n,s,t) -> C.Prod (n, letin_nf s, letin_nf t) | C.Lambda (n,s,t) -> C.Lambda (n, letin_nf s, letin_nf t) - | C.LetIn (n,s,t) -> CicSubstitution.subst (letin_nf s) t + | C.LetIn (n,s,_,t) -> CicSubstitution.subst (letin_nf s) t | C.Appl l -> C.Appl (List.map letin_nf l) | C.Const (uri,exp_named_subst) -> let exp_named_subst' = diff --git a/helm/software/components/cic_proof_checking/cicPp.ml b/helm/software/components/cic_proof_checking/cicPp.ml index 8c37c0f93..1686cd357 100644 --- a/helm/software/components/cic_proof_checking/cicPp.ml +++ b/helm/software/components/cic_proof_checking/cicPp.ml @@ -126,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 @@ -278,9 +278,7 @@ let ppcontext ?metasenv ?(sep = "\n") 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 ?metasenv ty 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 @@ -318,18 +316,19 @@ let ppobj obj = (fun context_entry (i,name_context) -> (match context_entry with Some (n,C.Decl at) -> - (separate i) ^ - ppname n ^ ":" ^ - pp ~metasenv:conjectures at name_context ^ " ", - (Some n)::name_context - | Some (n,C.Def (at,None)) -> - (separate i) ^ - ppname n ^ ":= " ^ pp ~metasenv:conjectures - 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) ^ ": " ^ @@ -421,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 -> diff --git a/helm/software/components/cic_proof_checking/cicReduction.ml b/helm/software/components/cic_proof_checking/cicReduction.ml index 532d0dc1e..32ae57a47 100644 --- a/helm/software/components/cic_proof_checking/cicReduction.ml +++ b/helm/software/components/cic_proof_checking/cicReduction.ml @@ -451,7 +451,8 @@ debug_print (lazy ("%%%%%UWVAR " ^ String.concat " ; " (List.map (function (uri, | C.Cast (te,ty) -> C.Cast (unwind_aux m te, unwind_aux m ty) (*CSC ???*) | C.Prod (n,s,t) -> C.Prod (n, unwind_aux m s, unwind_aux (m + 1) t) | C.Lambda (n,s,t) -> C.Lambda (n, unwind_aux m s, unwind_aux (m + 1) t) - | C.LetIn (n,s,t) -> C.LetIn (n, unwind_aux m s, unwind_aux (m + 1) t) + | C.LetIn (n,s,ty,t) -> + C.LetIn (n, unwind_aux m s, unwind_aux m ty, unwind_aux (m + 1) t) | C.Appl l -> C.Appl (List.map (unwind_aux m) l) | C.Const (uri,exp_named_subst) -> let params = @@ -645,7 +646,7 @@ if List.mem uri params then debug_print (lazy "---- OK2") ; | (_, _, _, C.Lambda _, []) as config -> config | (k, e, ens, C.Lambda (_,_,t), p::s) -> reduce (k+1, (RS.stack_to_env ~reduce ~unwind p)::e, ens, t,s) - | (k, e, ens, C.LetIn (_,m,t), s) -> + | (k, e, ens, C.LetIn (_,m,_,t), s) -> let m' = RS.compute_to_env ~reduce ~unwind k e ens m in reduce (k+1, m'::e, ens, t, s) | (_, _, _, C.Appl [], _) -> assert false @@ -914,11 +915,15 @@ prerr_endline ("%%%%%%: " ^ CicPp.ppterm term' ^ " <==> " ^ CicPp.ppterm t1); t1 t2 ugraph' else false,ugraph - | (C.LetIn (name1,s1,t1), C.LetIn(_,s2,t2)) -> + | (C.LetIn (name1,s1,ty1,t1), C.LetIn(_,s2,ty2,t2)) -> let b',ugraph' = aux test_equality_only context s1 s2 ugraph in if b' then - aux test_equality_only - ((Some (name1, (C.Def (s1,None))))::context) t1 t2 ugraph' + let b',ugraph = aux test_equality_only context ty1 ty2 ugraph in + if b' then + aux test_equality_only + ((Some (name1, (C.Def (s1,ty1))))::context) t1 t2 ugraph' + else + false,ugraph else false,ugraph | (C.Appl l1, C.Appl l2) -> @@ -1171,7 +1176,7 @@ let rec normalize ?(delta=true) ?(subst=[]) ctx term = | C.Lambda (n,s,t) -> let s' = aux ctx s in C.Lambda (n, s', aux ((decl n s')::ctx) t) - | C.LetIn (n,s,t) -> + | C.LetIn (n,s,_,t) -> (* the term is already in weak head normal form *) assert false | C.Appl (h::l) -> C.Appl (h::(List.map (aux ctx) l)) diff --git a/helm/software/components/cic_proof_checking/cicSubstitution.ml b/helm/software/components/cic_proof_checking/cicSubstitution.ml index a4340583e..4f888a3a5 100644 --- a/helm/software/components/cic_proof_checking/cicSubstitution.ml +++ b/helm/software/components/cic_proof_checking/cicSubstitution.ml @@ -62,7 +62,8 @@ let lift_from k n = | C.Cast (te,ty) -> C.Cast (liftaux k te, liftaux k ty) | C.Prod (n,s,t) -> C.Prod (n, liftaux k s, liftaux (k+1) t) | C.Lambda (n,s,t) -> C.Lambda (n, liftaux k s, liftaux (k+1) t) - | C.LetIn (n,s,t) -> C.LetIn (n, liftaux k s, liftaux (k+1) t) + | C.LetIn (n,s,ty,t) -> + C.LetIn (n, liftaux k s, liftaux k ty, liftaux (k+1) t) | C.Appl l -> C.Appl (List.map (liftaux k) l) | C.Const (uri,exp_named_subst) -> let exp_named_subst' = @@ -142,7 +143,8 @@ let rec subst ?(avoid_beta_redexes=false) arg = | C.Cast (te,ty) -> C.Cast (substaux k te, substaux k ty) | C.Prod (n,s,t) -> C.Prod (n, substaux k s, substaux (k + 1) t) | C.Lambda (n,s,t) -> C.Lambda (n, substaux k s, substaux (k + 1) t) - | C.LetIn (n,s,t) -> C.LetIn (n, substaux k s, substaux (k + 1) t) + | C.LetIn (n,s,ty,t) -> + C.LetIn (n, substaux k s, substaux k ty, substaux (k + 1) t) | C.Appl (he::tl) -> (* Invariant: no Appl applied to another Appl *) let tl' = List.map (substaux k) tl in @@ -257,7 +259,8 @@ debug_print (lazy "---- END\n\n ") ; | C.Cast (te,ty) -> C.Cast (substaux k te, substaux k ty) | C.Prod (n,s,t) -> C.Prod (n, substaux k s, substaux (k + 1) t) | C.Lambda (n,s,t) -> C.Lambda (n, substaux k s, substaux (k + 1) t) - | C.LetIn (n,s,t) -> C.LetIn (n, substaux k s, substaux (k + 1) t) + | C.LetIn (n,s,ty,t) -> + C.LetIn (n, substaux k s, substaux k ty, substaux (k + 1) t) | C.Appl (he::tl) -> (* Invariant: no Appl applied to another Appl *) let tl' = List.map (substaux k) tl in @@ -398,7 +401,7 @@ let subst_meta l t = | C.Cast (te,ty) -> C.Cast (aux k te, aux k ty) (*CSC ??? *) | C.Prod (n,s,t) -> C.Prod (n, aux k s, aux (k + 1) t) | C.Lambda (n,s,t) -> C.Lambda (n, aux k s, aux (k + 1) t) - | C.LetIn (n,s,t) -> C.LetIn (n, aux k s, aux (k + 1) t) + | C.LetIn (n,s,ty,t) -> C.LetIn (n, aux k s, aux k ty, aux (k + 1) t) | C.Appl l -> C.Appl (List.map (aux k) l) | C.Const (uri,exp_named_subst) -> let exp_named_subst' = diff --git a/helm/software/components/cic_proof_checking/cicTypeChecker.ml b/helm/software/components/cic_proof_checking/cicTypeChecker.ml index fbb384d5e..c23555494 100644 --- a/helm/software/components/cic_proof_checking/cicTypeChecker.ml +++ b/helm/software/components/cic_proof_checking/cicTypeChecker.ml @@ -75,7 +75,7 @@ let debrujin_constructor ?(cb=fun _ _ -> ()) uri number_of_types = | C.Cast (te,ty) -> C.Cast (aux k te, aux k ty) | C.Prod (n,s,t) -> C.Prod (n, aux k s, aux (k+1) t) | C.Lambda (n,s,t) -> C.Lambda (n, aux k s, aux (k+1) t) - | C.LetIn (n,s,t) -> C.LetIn (n, aux k s, aux (k+1) t) + | C.LetIn (n,s,ty,t) -> C.LetIn (n, aux k s, aux k ty, aux (k+1) t) | C.Appl l -> C.Appl (List.map (aux k) l) | C.Const (uri,exp_named_subst) -> let exp_named_subst' = @@ -273,10 +273,11 @@ and does_not_occur ?(subst=[]) context n nn te = does_not_occur ~subst context n nn so && does_not_occur ~subst ((Some (name,(C.Decl so)))::context) (n + 1) (nn + 1) dest - | C.LetIn (name,so,dest) -> + | C.LetIn (name,so,ty,dest) -> does_not_occur ~subst context n nn so && - does_not_occur ~subst ((Some (name,(C.Def (so,None))))::context) - (n + 1) (nn + 1) dest + does_not_occur ~subst context n nn ty && + does_not_occur ~subst ((Some (name,(C.Def (so,ty))))::context) + (n + 1) (nn + 1) dest | C.Appl l -> List.fold_right (fun x i -> i && does_not_occur ~subst context n nn x) l true | C.Var (_,exp_named_subst) @@ -765,9 +766,10 @@ and check_is_really_smaller_arg ~subst context n nn kl x safes te = check_is_really_smaller_arg ~subst context n nn kl x safes so && check_is_really_smaller_arg ~subst ((Some (name,(C.Decl so)))::context) (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta - | C.LetIn (name,so,ta) -> + | C.LetIn (name,so,ty,ta) -> check_is_really_smaller_arg ~subst context n nn kl x safes so && - check_is_really_smaller_arg ~subst ((Some (name,(C.Def (so,None))))::context) + check_is_really_smaller_arg ~subst context n nn kl x safes ty && + check_is_really_smaller_arg ~subst ((Some (name,(C.Def (so,ty))))::context) (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta | C.Appl (he::_) -> (*CSC: sulla coda ci vogliono dei controlli? secondo noi no, ma *) @@ -953,10 +955,11 @@ and guarded_by_destructors ~subst context n nn kl x safes = guarded_by_destructors ~subst context n nn kl x safes so && guarded_by_destructors ~subst ((Some (name,(C.Decl so)))::context) (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta - | C.LetIn (name,so,ta) -> + | C.LetIn (name,so,ty,ta) -> guarded_by_destructors ~subst context n nn kl x safes so && - guarded_by_destructors ~subst ((Some (name,(C.Def (so,None))))::context) - (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta + guarded_by_destructors ~subst context n nn kl x safes ty && + guarded_by_destructors ~subst ((Some (name,(C.Def (so,ty))))::context) + (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta | C.Appl ((C.Rel m)::tl) when m > n && m <= nn -> let k = List.nth kl (m - n - 1) in if not (List.length tl > k) then false @@ -1491,11 +1494,9 @@ and check_metasenv_consistency ~logger ~subst metasenv context [] -> [] | (Some (n,C.Decl t))::tl -> (Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl) - | (Some (n,C.Def (t,None)))::tl -> - (Some (n,C.Def ((S.subst_meta l (S.lift i t)),None)))::(aux (i+1) tl) | None::tl -> None::(aux (i+1) tl) - | (Some (n,C.Def (t,Some ty)))::tl -> - (Some (n,C.Def ((S.subst_meta l (S.lift i t)),Some (S.subst_meta l (S.lift i ty)))))::(aux (i+1) tl) + | (Some (n,C.Def (t,ty)))::tl -> + (Some (n,C.Def ((S.subst_meta l (S.lift i t)),S.subst_meta l (S.lift i ty))))::(aux (i+1) tl) in aux 1 canonical_context in @@ -1567,10 +1568,7 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = (try match List.nth context (n - 1) with Some (_,C.Decl t) -> S.lift n t,ugraph - | Some (_,C.Def (_,Some ty)) -> S.lift n ty,ugraph - | Some (_,C.Def (bo,None)) -> - debug_print (lazy "##### CASO DA INVESTIGARE E CAPIRE") ; - type_of_aux ~logger context (S.lift n bo) ugraph + | Some (_,C.Def (_,ty)) -> S.lift n ty,ugraph | None -> raise (TypeCheckerFailure (lazy "Reference to deleted hypothesis")) with @@ -1645,9 +1643,19 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = type_of_aux ~logger ((Some (n,(C.Decl s)))::context) t ugraph1 in (C.Prod (n,s,type2)),ugraph2 - | C.LetIn (n,s,t) -> + | C.LetIn (n,s,ty,t) -> (* only to check if s is well-typed *) - let ty,ugraph1 = type_of_aux ~logger context s ugraph in + let ty',ugraph1 = type_of_aux ~logger context s ugraph in + let b,ugraph1 = + R.are_convertible ~subst ~metasenv context ty ty' ugraph1 + in + if not b then + raise + (TypeCheckerFailure + (lazy (sprintf + "The type of %s is %s but it is expected to be %s" + (CicPp.ppterm s) (CicPp.ppterm ty') (CicPp.ppterm ty)))) + else (* The type of a LetIn is a LetIn. Extremely slow since the computed LetIn is later reduced and maybe also re-checked. (C.LetIn (n,s, type_of_aux ((Some (n,(C.Def s)))::context) t)) @@ -1662,7 +1670,7 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = Moreover the inferred type is closer to the expected one. *) let ty1,ugraph2 = type_of_aux ~logger - ((Some (n,(C.Def (s,Some ty))))::context) t ugraph1 + ((Some (n,(C.Def (s,ty))))::context) t ugraph1 in (CicSubstitution.subst ~avoid_beta_redexes:true s ty1),ugraph2 | C.Appl (he::tl) when List.length tl > 0 -> diff --git a/helm/software/components/cic_proof_checking/cicUnivUtils.ml b/helm/software/components/cic_proof_checking/cicUnivUtils.ml index cbc87e98a..d61545ff6 100644 --- a/helm/software/components/cic_proof_checking/cicUnivUtils.ml +++ b/helm/software/components/cic_proof_checking/cicUnivUtils.ml @@ -85,7 +85,7 @@ let universes_of_obj uri t = | C.Cast (v,t) -> C.Cast (aux v, aux t) | C.Prod (b,s,t) -> C.Prod (b,aux s, aux t) | C.Lambda (b,s,t) -> C.Lambda (b,aux s, aux t) - | C.LetIn (b,s,t) -> C.LetIn (b,aux s, aux t) + | C.LetIn (b,s,ty,t) -> C.LetIn (b,aux s, aux ty, aux t) | C.Appl li -> C.Appl (List.map aux li) | C.MutCase (uri,n1,ty,te,patterns) -> C.MutCase (uri,n1,aux ty,aux te, List.map aux patterns) diff --git a/helm/software/components/cic_proof_checking/freshNamesGenerator.ml b/helm/software/components/cic_proof_checking/freshNamesGenerator.ml index 73b75ce18..1cb86b35a 100755 --- a/helm/software/components/cic_proof_checking/freshNamesGenerator.ml +++ b/helm/software/components/cic_proof_checking/freshNamesGenerator.ml @@ -63,7 +63,7 @@ let rec guess_a_name context ty = (* warning: on appl we should beta reduce before the recursive call | Cic.Lambda _ -> assert false *) - | Cic.LetIn (_,s,t) -> guess_a_name context (CicSubstitution.subst ~avoid_beta_redexes:true s t) + | Cic.LetIn (_,s,_,t) -> guess_a_name context (CicSubstitution.subst ~avoid_beta_redexes:true s t) | Cic.Appl [] -> assert false | Cic.Appl (he::_) -> guess_a_name context he | Cic.Const (uri,_) @@ -157,16 +157,17 @@ let rec mk_fresh_names ~subst metasenv context t = | _ -> n in let t' = mk_fresh_names ~subst metasenv (Some(n',Cic.Decl s')::context) t in Cic.Lambda (n',s',t') - | Cic.LetIn (n,s,t) -> + | Cic.LetIn (n,s,ty,t) -> let s' = mk_fresh_names ~subst metasenv context s in + let ty' = mk_fresh_names ~subst metasenv context ty in let n' = match n with Cic.Anonymous -> Cic.Anonymous | Cic.Name "matita_dummy" -> mk_fresh_name ~subst metasenv context Cic.Anonymous ~typ:s' | _ -> n in - let t' = mk_fresh_names ~subst metasenv (Some(n',Cic.Def (s',None))::context) t in - Cic.LetIn (n',s',t') + let t' = mk_fresh_names ~subst metasenv (Some(n',Cic.Def (s',ty'))::context) t in + Cic.LetIn (n',s',ty',t') | Cic.Appl l -> Cic.Appl (List.map (mk_fresh_names ~subst metasenv context) l) | Cic.Const (uri,exp_named_subst) -> @@ -282,12 +283,13 @@ let clean_dummy_dependent_types t = let s',rels1 = aux k s in let t',rels2 = aux (k+1) t in C.Lambda (n, s', t'), rels1@rels2 - | C.LetIn (n,s,t) -> + | C.LetIn (n,s,ty,t) -> let s',rels1 = aux k s in - let t',rels2 = aux (k+1) t in - let rels = rels1 @ rels2 in - if List.mem k rels2 then - C.LetIn (n, s', t'), rels + let ty',rels2 = aux k ty in + let t',rels3 = aux (k+1) t in + let rels = rels1 @ rels2 @ rels3 in + if List.mem k rels3 then + C.LetIn (n, s', ty', t'), rels else (* (C.Rel 1) is just a dummy term; any term would fit *) CicSubstitution.subst (C.Rel 1) t', rels diff --git a/helm/software/components/cic_unification/cicMetaSubst.ml b/helm/software/components/cic_unification/cicMetaSubst.ml index 070a07c93..91368cde9 100644 --- a/helm/software/components/cic_unification/cicMetaSubst.ml +++ b/helm/software/components/cic_unification/cicMetaSubst.ml @@ -198,7 +198,7 @@ let apply_subst_gen ~appl_fun subst term = | C.Cast (te,ty) -> C.Cast (um_aux te, um_aux ty) | C.Prod (n,s,t) -> C.Prod (n, um_aux s, um_aux t) | C.Lambda (n,s,t) -> C.Lambda (n, um_aux s, um_aux t) - | C.LetIn (n,s,t) -> C.LetIn (n, um_aux s, um_aux t) + | C.LetIn (n,s,ty,t) -> C.LetIn (n, um_aux s, um_aux ty, um_aux t) | C.Appl (hd :: tl) -> appl_fun um_aux hd tl | C.Appl _ -> assert false | C.Const (uri,exp_named_subst) -> @@ -274,11 +274,7 @@ let apply_subst_context subst context = let t' = apply_subst subst t in Some (n, Cic.Decl t') :: context | Some (n, Cic.Def (t, ty)) -> - let ty' = - match ty with - | None -> None - | Some ty -> Some (apply_subst subst ty) - in + let ty' = apply_subst subst ty in let t' = apply_subst subst t in Some (n, Cic.Def (t', ty')) :: context | None -> None :: context) @@ -335,9 +331,7 @@ let ppcontext' ~metasenv ?(sep = "\n") subst context = (Some n)::name_context | Some (n,Cic.Def (bo,ty)) -> sprintf "%s%s : %s := %s" (separate i) (CicPp.ppname n) - (match ty with - None -> "_" - | Some ty -> ppterm_in_name_context ~metasenv subst ty name_context) + (ppterm_in_name_context ~metasenv subst ty name_context) (ppterm_in_name_context ~metasenv subst bo name_context), (Some n)::name_context | None -> sprintf "%s_ :? _" (separate i), None::name_context @@ -443,7 +437,8 @@ let rec force_does_not_occur subst to_be_restricted t = | C.Cast (te,ty) -> C.Cast (aux k te, aux k ty) | C.Prod (name,so,dest) -> C.Prod (name, aux k so, aux (k+1) dest) | C.Lambda (name,so,dest) -> C.Lambda (name, aux k so, aux (k+1) dest) - | C.LetIn (name,so,dest) -> C.LetIn (name, aux k so, aux (k+1) dest) + | C.LetIn (name,so,ty,dest) -> + C.LetIn (name, aux k so, aux k ty, aux (k+1) dest) | C.Appl l -> C.Appl (List.map (aux k) l) | C.Var (uri,exp_named_subst) -> let exp_named_subst' = @@ -515,14 +510,11 @@ let rec restrict subst to_be_restricted metasenv = force_does_not_occur subst to_be_restricted bo in let more_to_be_restricted, ty' = - match ty with - | None -> more_to_be_restricted, None - | Some ty -> - let more_to_be_restricted', ty' = - force_does_not_occur subst to_be_restricted ty - in - more_to_be_restricted @ more_to_be_restricted', - Some ty' + let more_to_be_restricted', ty' = + force_does_not_occur subst to_be_restricted ty + in + more_to_be_restricted @ more_to_be_restricted', + ty' in more_to_be_restricted, Some (name, Cic.Def (bo', ty')) in @@ -712,7 +704,8 @@ let delift n subst context metasenv l t = | C.Cast (te,ty) -> C.Cast (deliftaux k te, deliftaux k ty) | C.Prod (n,s,t) -> C.Prod (n, deliftaux k s, deliftaux (k+1) t) | C.Lambda (n,s,t) -> C.Lambda (n, deliftaux k s, deliftaux (k+1) t) - | C.LetIn (n,s,t) -> C.LetIn (n, deliftaux k s, deliftaux (k+1) t) + | C.LetIn (n,s,ty,t) -> + C.LetIn (n, deliftaux k s, deliftaux k ty, deliftaux (k+1) t) | C.Appl l -> C.Appl (List.map (deliftaux k) l) | C.Const (uri,exp_named_subst) -> let exp_named_subst' = @@ -853,10 +846,11 @@ let delift_rels_from subst metasenv k n = let s',subst,metasenv = liftaux subst metasenv k s in let t',subst,metasenv = liftaux subst metasenv (k+1) t in C.Lambda (n,s',t'),subst,metasenv - | C.LetIn (n,s,t) -> + | C.LetIn (n,s,ty,t) -> let s',subst,metasenv = liftaux subst metasenv k s in + let ty',subst,metasenv = liftaux subst metasenv k ty in let t',subst,metasenv = liftaux subst metasenv (k+1) t in - C.LetIn (n,s',t'),subst,metasenv + C.LetIn (n,s',ty',t'),subst,metasenv | C.Appl l -> let l',subst,metasenv = List.fold_right diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml index 318d1e742..dd5191a15 100644 --- a/helm/software/components/cic_unification/cicRefine.ml +++ b/helm/software/components/cic_unification/cicRefine.ml @@ -337,15 +337,8 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t match List.nth context (n - 1) with Some (_,C.Decl ty) -> t,S.lift n ty,subst,metasenv, ugraph - | Some (_,C.Def (_,Some ty)) -> + | Some (_,C.Def (_,ty)) -> t,S.lift n ty,subst,metasenv, ugraph - | Some (_,C.Def (bo,None)) -> - let ty,ugraph = - (* if it is in the context it must be already well-typed*) - CicTypeChecker.type_of_aux' ~subst metasenv context - (S.lift n bo) ugraph - in - t,ty,subst,metasenv,ugraph | None -> enrich localization_tbl t (RefineFailure (lazy "Rel to hidden hypothesis")) @@ -445,12 +438,29 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t in C.Lambda (n,s',t'),C.Prod (n,s',type2), subst'',metasenv'',ugraph2 - | C.LetIn (n,s,t) -> - (* only to check if s is well-typed *) - let s',ty,subst',metasenv',ugraph1 = - type_of_aux subst metasenv context s ugraph - in - let context_for_t = ((Some (n,(C.Def (s',Some ty))))::context) in + | C.LetIn (n,s,ty,t) -> + (* only to check if s is well-typed *) + let s',ty',subst',metasenv',ugraph1 = + type_of_aux subst metasenv context s ugraph in + let ty,_,subst',metasenv',ugraph1 = + type_of_aux subst' metasenv' context ty ugraph1 in + let subst',metasenv',ugraph1 = + try + fo_unif_subst subst' context metasenv' + ty ty' ugraph1 + with + exn -> + enrich localization_tbl s' exn + ~f:(function _ -> + lazy ("The term " ^ + CicMetaSubst.ppterm_in_context ~metasenv:metasenv' subst' s' + context ^ " has type " ^ + CicMetaSubst.ppterm_in_context ~metasenv:metasenv' subst' ty' + context ^ " but is here used with type " ^ + CicMetaSubst.ppterm_in_context ~metasenv:metasenv' subst' ty + context)) + in + let context_for_t = ((Some (n,(C.Def (s',ty))))::context) in let t',inferredty,subst'',metasenv'',ugraph2 = type_of_aux subst' metasenv' @@ -460,7 +470,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t * Even faster than the previous solution. * Moreover the inferred type is closer to the expected one. *) - C.LetIn (n,s',t'), + C.LetIn (n,s',ty,t'), CicSubstitution.subst ~avoid_beta_redexes:true s' inferredty, subst'',metasenv'',ugraph2 | C.Appl (he::((_::_) as tl)) -> @@ -939,13 +949,13 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t [] -> [] | (Some (n,C.Decl t))::tl -> (Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl) - | (Some (n,C.Def (t,None)))::tl -> - (Some (n,C.Def ((S.subst_meta l (S.lift i t)),None)))::(aux (i+1) tl) | None::tl -> None::(aux (i+1) tl) - | (Some (n,C.Def (t,Some ty)))::tl -> - (Some (n, - C.Def ((S.subst_meta l (S.lift i t)), - Some (S.subst_meta l (S.lift i ty))))) :: (aux (i+1) tl) + | (Some (n,C.Def (t,ty)))::tl -> + (Some + (n, + C.Def + (S.subst_meta l (S.lift i t), + S.subst_meta l (S.lift i ty)))) :: (aux (i+1) tl) in aux 1 canonical_context in @@ -1751,11 +1761,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t Cic.Decl (FreshNamesGenerator.clean_dummy_dependent_types t)) | Some (n, Cic.Def (bo,ty)) -> let bo' = FreshNamesGenerator.clean_dummy_dependent_types bo in - let ty' = - match ty with - None -> None - | Some ty -> - Some (FreshNamesGenerator.clean_dummy_dependent_types ty) + let ty' = FreshNamesGenerator.clean_dummy_dependent_types ty in Some (n, Cic.Def (bo',ty')) ) context @@ -1972,13 +1978,11 @@ let pack_coercion metasenv ctx t = | C.Lambda (name,so,dest) -> let ctx' = (Some (name,C.Decl so))::ctx in C.Lambda (name, merge_coercions ctx so, merge_coercions ctx' dest) - | C.LetIn (name,so,dest) -> - let _,ty,metasenv,ugraph = - pack_coercions := false; - type_of_aux' metasenv ctx so CicUniv.oblivion_ugraph in - pack_coercions := true; - let ctx' = Some (name,(C.Def (so,Some ty)))::ctx in - C.LetIn (name, merge_coercions ctx so, merge_coercions ctx' dest) + | C.LetIn (name,so,ty,dest) -> + let ctx' = Some (name,(C.Def (so,ty)))::ctx in + C.LetIn + (name, merge_coercions ctx so, merge_coercions ctx ty, + merge_coercions ctx' dest) | C.Appl l -> let l = List.map (merge_coercions ctx) l in let t = C.Appl l in diff --git a/helm/software/components/cic_unification/cicReplace.ml b/helm/software/components/cic_unification/cicReplace.ml index 7f53e1ee5..0b8b67497 100644 --- a/helm/software/components/cic_unification/cicReplace.ml +++ b/helm/software/components/cic_unification/cicReplace.ml @@ -42,7 +42,7 @@ let replace_lifting ~equality ~context ~what ~with_what ~where = find_image_aux (what,with_what) in let add_ctx ctx n s = (Some (n, Cic.Decl s))::ctx in - let add_ctx1 ctx n s = (Some (n, Cic.Def (s,None)))::ctx in + let add_ctx1 ctx n s ty = (Some (n, Cic.Def (s,ty)))::ctx in let rec substaux k ctx what t = try S.lift (k-1) (find_image ctx what t) @@ -72,9 +72,9 @@ let replace_lifting ~equality ~context ~what ~with_what ~where = | C.Lambda (n,s,t) -> C.Lambda (n, substaux k ctx what s, substaux (k + 1) (add_ctx ctx n s) (List.map (S.lift 1) what) t) - | C.LetIn (n,s,t) -> + | C.LetIn (n,s,ty,t) -> C.LetIn - (n, substaux k ctx what s, substaux (k + 1) (add_ctx1 ctx n s) (List.map (S.lift 1) what) t) + (n, substaux k ctx what s, substaux k ctx what ty, substaux (k + 1) (add_ctx1 ctx n s ty) (List.map (S.lift 1) what) t) | C.Appl (he::tl) -> (* Invariant: no Appl applied to another Appl *) let tl' = List.map (substaux k ctx what) tl in diff --git a/helm/software/components/cic_unification/cicUnification.ml b/helm/software/components/cic_unification/cicUnification.ml index fb6a66d4f..8044878b2 100644 --- a/helm/software/components/cic_unification/cicUnification.ml +++ b/helm/software/components/cic_unification/cicUnification.ml @@ -197,15 +197,17 @@ let foo () = in (* TASSI: sure this is in serial? *) subst,metasenv,(C.Lambda (nn, s', t')),ugraph2 - | C.LetIn (nn,s,t) -> + | C.LetIn (nn,s,ty,t) -> let subst,metasenv,s',ugraph1 = aux metasenv subst n context s ugraph in + let subst,metasenv,ty',ugraph1 = + aux metasenv subst n context ty ugraph in let subst,metasenv,t',ugraph2 = - aux metasenv subst (n+1) ((Some (nn, C.Def (s,None)))::context) t + aux metasenv subst (n+1) ((Some (nn, C.Def (s,ty)))::context) t ugraph1 in (* TASSI: sure this is in serial? *) - subst,metasenv,(C.LetIn (nn, s', t')),ugraph2 + subst,metasenv,(C.LetIn (nn, s', ty', t')),ugraph2 | C.Appl l -> let subst,metasenv,revl',ugraph1 = List.fold_left @@ -508,8 +510,8 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ in fo_unif_subst test_equality_only subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1 - | (C.LetIn (_,s1,t1), t2) - | (t2, C.LetIn (_,s1,t1)) -> + | (C.LetIn (_,s1,ty1,t1), t2) + | (t2, C.LetIn (_,s1,ty1,t1)) -> fo_unif_subst test_equality_only subst context metasenv t2 (S.subst s1 t1) ugraph | (C.Appl l1, C.Appl l2) -> diff --git a/helm/software/components/content_pres/termContentPres.ml b/helm/software/components/content_pres/termContentPres.ml index d68b6a8b4..0f51e36a9 100644 --- a/helm/software/components/content_pres/termContentPres.ml +++ b/helm/software/components/content_pres/termContentPres.ml @@ -204,7 +204,8 @@ let pp_ast0 t k = hvbox false true [ keyword "let"; space; hvbox false true [ - aux_var var; space; builtin_symbol "\\def"; break; top_pos (k s) ]; + aux_var var; space; + builtin_symbol "\\def"; break; top_pos (k s) ]; break; space; keyword "in" ]; break; k t ]) @@ -550,8 +551,8 @@ let instantiate_level2 env term = | Ast.Case (term, indty, outty_opt, patterns) -> Ast.Case (aux env term, indty, aux_opt env outty_opt, List.map (aux_branch env) patterns) - | Ast.LetIn (var, t1, t2) -> - Ast.LetIn (aux_capture_var env var, aux env t1, aux env t2) + | Ast.LetIn (var, t1, t3) -> + Ast.LetIn (aux_capture_var env var, aux env t1, aux env t3) | Ast.LetRec (kind, definitions, body) -> Ast.LetRec (kind, List.map (aux_definition env) definitions, aux env body) diff --git a/helm/software/components/metadata/metadataConstraints.ml b/helm/software/components/metadata/metadataConstraints.ml index 73f137a43..e35e35894 100644 --- a/helm/software/components/metadata/metadataConstraints.ml +++ b/helm/software/components/metadata/metadataConstraints.ml @@ -269,8 +269,9 @@ and inspect_conclusion n t = merge n (inspect_conclusion n s) (inspect_conclusion n t) | Cic.Lambda (_, s, t) -> merge n (inspect_conclusion n s) (inspect_conclusion n t) - | Cic.LetIn (_, s, t) -> - merge n (inspect_conclusion n s) (inspect_conclusion n t) + | Cic.LetIn (_, s, ty, t) -> + merge n (inspect_conclusion n s) + (merge n (inspect_conclusion n ty) (inspect_conclusion n t)) | Cic.Appl ((Cic.Const (u,exp_named_subst))::l) -> add_root (n-1) u l | Cic.Appl ((Cic.MutInd (u, t, exp_named_subst))::l) -> @@ -308,7 +309,7 @@ let rec inspect_term n t = Some uri, SetSet.empty | Cic.Cast (t, _) -> inspect_term n t | Cic.Prod (_, _, t) -> inspect_term n t - | Cic.LetIn (_, _, t) -> inspect_term n t + | Cic.LetIn (_, _, _, t) -> inspect_term n t | Cic.Appl ((Cic.Const (u,exp_named_subst))::l) -> let childunion = inspect_children (n-1) l in Some u, childunion @@ -396,8 +397,9 @@ and signature_concl = UriManagerSet.union (signature_concl s) (signature_concl t) | Cic.Lambda (_, s, t) -> UriManagerSet.union (signature_concl s) (signature_concl t) - | Cic.LetIn (_, s, t) -> - UriManagerSet.union (signature_concl s) (signature_concl t) + | Cic.LetIn (_, s, ty, t) -> + UriManagerSet.union (signature_concl s) + (UriManagerSet.union (signature_concl ty) (signature_concl t)) | Cic.Appl l -> add l | Cic.MutCase _ | Cic.Fix _ @@ -407,7 +409,7 @@ and signature_concl = let rec signature_of = function | Cic.Cast (t, _) -> signature_of t | Cic.Prod (_, _, t) -> signature_of t - | Cic.LetIn (_, _, t) -> signature_of t + | Cic.LetIn (_, _, _, t) -> signature_of t | Cic.Appl ((Cic.Const (u,exp_named_subst))::l) -> Some (u, []), add l | Cic.Appl ((Cic.MutInd (u, t, exp_named_subst))::l) -> diff --git a/helm/software/components/metadata/metadataExtractor.ml b/helm/software/components/metadata/metadataExtractor.ml index 4fbae1ba7..462679534 100644 --- a/helm/software/components/metadata/metadataExtractor.ml +++ b/helm/software/components/metadata/metadataExtractor.ml @@ -119,7 +119,7 @@ let compute_term pos term = (*assert (not (is_main_pos pos));*) let set = aux (next_pos pos) set source in aux (next_pos pos) set target - | Cic.LetIn (_, term, target) -> + | Cic.LetIn (_, term, _, target) -> if is_main_pos pos then aux pos set (CicSubstitution.subst term target) else @@ -210,7 +210,7 @@ let compute_metas term = | Cic.Lambda (_, source, target) -> let acc = aux in_hyp acc source in aux in_hyp acc target - | Cic.LetIn (_, term, target) -> + | Cic.LetIn (_, term, _, target) -> aux in_hyp acc (CicSubstitution.subst term target) | Cic.Appl [] -> assert false | Cic.Appl (hd :: tl) -> diff --git a/helm/software/components/tactics/auto.ml b/helm/software/components/tactics/auto.ml index ba80608d2..9be698dcf 100644 --- a/helm/software/components/tactics/auto.ml +++ b/helm/software/components/tactics/auto.ml @@ -69,7 +69,7 @@ let lambda_close ?prefix_name t menv ctx = (fun (t,i) -> function | None -> CicSubstitution.subst (Cic.Implicit None) t,i (* delift *) | Some (name, Cic.Decl ty) -> Cic.Lambda (name, ty, t),i+1 - | Some (name, Cic.Def (bo, _)) -> Cic.LetIn (name, bo, t),i+1) + | Some (name, Cic.Def (bo, ty)) -> Cic.LetIn (name, bo, ty, t),i+1) (t,List.length menv) ctx ;; @@ -98,16 +98,9 @@ let find_context_theorems context metasenv = match ctxentry with | Some (_,Cic.Decl t) -> (Cic.Rel i, CicSubstitution.lift i t)::res,i+1 - | Some (_,Cic.Def (_,Some t)) -> + | Some (_,Cic.Def (_,t)) -> (Cic.Rel i, CicSubstitution.lift i t)::res,i+1 - | Some (_,Cic.Def (_,None)) -> - let t = Cic.Rel i in - let ty,_ = - CicTypeChecker.type_of_aux' - metasenv context t CicUniv.empty_ugraph - in - (t,ty)::res,i+1 - | _ -> res,i+1) + | None -> res,i+1) ([],1) context in l diff --git a/helm/software/components/tactics/fourierR.ml b/helm/software/components/tactics/fourierR.ml index 8e443447a..484497803 100644 --- a/helm/software/components/tactics/fourierR.ml +++ b/helm/software/components/tactics/fourierR.ml @@ -858,11 +858,9 @@ let rec superlift c n= [] -> [] | Some(name,Cic.Decl(a))::next -> [Some(name,Cic.Decl(CicSubstitution.lift n a))]@ superlift next (n+1) - | Some(name,Cic.Def(a,None))::next -> - [Some(name,Cic.Def((CicSubstitution.lift n a),None))]@ superlift next (n+1) - | Some(name,Cic.Def(a,Some ty))::next -> + | Some(name,Cic.Def(a,ty))::next -> [Some(name, - Cic.Def((CicSubstitution.lift n a),Some (CicSubstitution.lift n ty))) + Cic.Def((CicSubstitution.lift n a),CicSubstitution.lift n ty)) ] @ superlift next (n+1) | _::next -> superlift next (n+1) (*?? ??*) diff --git a/helm/software/components/tactics/paramodulation/equality.ml b/helm/software/components/tactics/paramodulation/equality.ml index 7893ecba6..2c1b30d67 100644 --- a/helm/software/components/tactics/paramodulation/equality.ml +++ b/helm/software/components/tactics/paramodulation/equality.ml @@ -323,8 +323,8 @@ Utils.debug_print (lazy ("!!! RISPARMIO " ^ string_of_int (List.length acc) ^ " remove_refl p1 | _ -> Cic.Appl (List.map remove_refl args)) | Cic.Appl l -> Cic.Appl (List.map remove_refl l) - | Cic.LetIn (name,bo,rest) -> - Cic.LetIn (name,remove_refl bo,remove_refl rest) + | Cic.LetIn (name,bo,ty,rest) -> + Cic.LetIn (name,remove_refl bo,remove_refl ty,remove_refl rest) | _ -> t in let rec canonical_trough_lambda context = function @@ -335,10 +335,11 @@ Utils.debug_print (lazy ("!!! RISPARMIO " ^ string_of_int (List.length acc) ^ " and canonical context t = match t with - | Cic.LetIn(name,bo,rest) -> + | Cic.LetIn(name,bo,ty,rest) -> let bo = canonical_trough_lambda context bo in - let context' = (Some (name,Cic.Def (bo,None)))::context in - Cic.LetIn(name,bo,canonical context' rest) + let ty = canonical_trough_lambda context ty in + let context' = (Some (name,Cic.Def (bo,ty)))::context in + Cic.LetIn(name,bo,ty,canonical context' rest) | Cic.Appl (((Cic.Const(uri_sym,ens))::tl) as args) when LibraryObjects.is_sym_eq_URI uri_sym -> (match p_of_sym ens tl with @@ -430,8 +431,10 @@ let contextualize uri ty left right t = when LibraryObjects.is_sym_eq_URI uri_sym -> let ty,l,r,p = open_sym ens tl in mk_sym uri_sym ty l r (aux uri ty l r ctx_d ctx_ty p) - | Cic.LetIn (name,body,rest) -> - Cic.LetIn (name,look_ahead (aux uri) body, aux uri ty left right ctx_d ctx_ty rest) + | Cic.LetIn (name,body,bodyty,rest) -> + Cic.LetIn + (name,look_ahead (aux uri) body, bodyty, + aux uri ty left right ctx_d ctx_ty rest) | Cic.Appl ((Cic.Const(uri_ind,ens))::tl) when LibraryObjects.is_eq_ind_URI uri_ind || LibraryObjects.is_eq_ind_r_URI uri_ind -> @@ -800,6 +803,16 @@ let build_goal_proof bag eq l initial ty se context menv = acc@[id,real_cic],n+1,h) ([],0,[]) lets in + let _,lets = + List.fold_left + (fun (context,res) (id,cic) -> + let ty,_ = + CicTypeChecker.type_of_aux' [] context cic CicUniv.oblivion_ugraph + in + Some (Cic.Name ("H" ^ string_of_int id), + Cic.Def (cic,ty))::context,res@[id,cic,ty] + ) (context,[]) lets + in let proof,se = let rec aux se current_proof = function | [] -> current_proof,se @@ -830,11 +843,13 @@ let build_goal_proof bag eq l initial ty se context menv = let n,proof = let initial = proof in List.fold_right - (fun (id,cic) (n,p) -> + (fun (id,cic,ty) (n,p) -> n-1, Cic.LetIn ( Cic.Name ("H"^string_of_int id), - cic, p)) + cic, + ty, + p)) lets (letsno-1,initial) in canonical @@ -944,9 +959,12 @@ let meta_convertibility_aux table t1 t2 = aux_ens table ens1 ens2 | C.Cast (s1, t1), C.Cast (s2, t2) | C.Prod (_, s1, t1), C.Prod (_, s2, t2) - | C.Lambda (_, s1, t1), C.Lambda (_, s2, t2) - | C.LetIn (_, s1, t1), C.LetIn (_, s2, t2) -> + | C.Lambda (_, s1, t1), C.Lambda (_, s2, t2) -> + let table = aux table s1 s2 in + aux table t1 t2 + | C.LetIn (_, s1, ty1, t1), C.LetIn (_, s2, ty2, t2) -> let table = aux table s1 s2 in + let table = aux table ty1 ty2 in aux table t1 t2 | C.Appl l1, C.Appl l2 -> ( try List.fold_left2 (fun res t1 t2 -> (aux res t1 t2)) table l1 l2 @@ -1201,7 +1219,7 @@ let rec pp_proofterm name t context = | _ -> assert false in let rec skip_letin ctx = function - | Cic.LetIn (n,b,t) -> + | Cic.LetIn (n,b,_,t) -> pp_proofterm (Some (rename "Lemma " n)) b ctx:: skip_letin ((Some n)::ctx) t | t -> diff --git a/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml index 9739f1ccf..5df1d7d6f 100644 --- a/helm/software/components/tactics/paramodulation/saturation.ml +++ b/helm/software/components/tactics/paramodulation/saturation.ml @@ -1277,10 +1277,11 @@ let fix_proof metasenv context all_implicits p = let metasenv,s = aux metasenv n s in let metasenv,t = aux metasenv (n+1) t in metasenv,Cic.Prod(name,s,t) - | Cic.LetIn(name,s,t) -> + | Cic.LetIn(name,s,ty,t) -> let metasenv,s = aux metasenv n s in + let metasenv,ty = aux metasenv n ty in let metasenv,t = aux metasenv (n+1) t in - metasenv,Cic.LetIn(name,s,t) + metasenv,Cic.LetIn(name,s,ty,t) | Cic.Const(uri,ens) -> let metasenv,ens = List.fold_right diff --git a/helm/software/components/tactics/paramodulation/subst.ml b/helm/software/components/tactics/paramodulation/subst.ml index 7e8ab8b18..fb8e3b78e 100644 --- a/helm/software/components/tactics/paramodulation/subst.ml +++ b/helm/software/components/tactics/paramodulation/subst.ml @@ -94,7 +94,7 @@ let naif_apply_subst lift subst term = | Cic.Cast (te,ty) -> Cic.Cast (aux k te, aux k ty) | Cic.Prod (n,s,t) -> Cic.Prod (n, aux k s, aux (k+1) t) | Cic.Lambda (n,s,t) -> Cic.Lambda (n, aux k s, aux (k+1) t) - | Cic.LetIn (n,s,t) -> Cic.LetIn (n, aux k s, aux (k+1) t) + | Cic.LetIn (n,s,ty,t) -> Cic.LetIn (n, aux k s, aux k ty, aux (k+1) t) | Cic.Appl [] -> assert false | Cic.Appl l -> Cic.Appl (List.map (aux k) l) | Cic.Const (uri,exp_named_subst) -> diff --git a/helm/software/components/tactics/paramodulation/utils.ml b/helm/software/components/tactics/paramodulation/utils.ml index c6e64b898..affd4897f 100644 --- a/helm/software/components/tactics/paramodulation/utils.ml +++ b/helm/software/components/tactics/paramodulation/utils.ml @@ -102,8 +102,8 @@ let metas_of_term term = TermSet.union (aux s) (aux t) | C.Prod(n,s,t) -> TermSet.union (aux s) (aux t) - | C.LetIn(n,s,t) -> - TermSet.union (aux s) (aux t) + | C.LetIn(n,s,ty,t) -> + TermSet.union (aux s) (TermSet.union (aux ty) (aux t)) | t -> TermSet.empty (* TODO: maybe add other cases? *) in aux term @@ -265,7 +265,7 @@ let weight_of_term ?(consider_metas=true) ?(count_metas_occurrences=false) term | C.Cast (t1, t2) | C.Lambda (_, t1, t2) | C.Prod (_, t1, t2) - | C.LetIn (_, t1, t2) -> + | C.LetIn (_, t1, _, t2) -> let w1 = aux t1 in let w2 = aux t2 in w1 + w2 + 1 diff --git a/helm/software/components/tactics/primitiveTactics.ml b/helm/software/components/tactics/primitiveTactics.ml index 2447fe1ef..e7632ebf4 100644 --- a/helm/software/components/tactics/primitiveTactics.ml +++ b/helm/software/components/tactics/primitiveTactics.ml @@ -62,11 +62,11 @@ let lambda_abstract ?(howmany=(-1)) metasenv context newmeta ty mk_fresh_name = collect_context ctx (howmany - 1) do_whd t in (context',ty,C.Lambda(n',s,bo)) - | C.LetIn (n,s,t) -> + | C.LetIn (n,s,sty,t) -> let (context',ty,bo) = - collect_context ((Some (n,(C.Def (s,None))))::context) (howmany - 1) do_whd t + collect_context ((Some (n,(C.Def (s,sty))))::context) (howmany - 1) do_whd t in - (context',ty,C.LetIn(n,s,bo)) + (context',ty,C.LetIn(n,s,sty,bo)) | _ as t -> if howmany <= 0 then let irl = @@ -102,7 +102,7 @@ let eta_expand metasenv context t arg = | C.Cast (te,ty) -> C.Cast (aux n te, aux n ty) | C.Prod (nn,s,t) -> C.Prod (nn, aux n s, aux (n+1) t) | C.Lambda (nn,s,t) -> C.Lambda (nn, aux n s, aux (n+1) t) - | C.LetIn (nn,s,t) -> C.LetIn (nn, aux n s, aux (n+1) t) + | C.LetIn (nn,s,ty,t) -> C.LetIn (nn, aux n s, aux n ty, aux (n+1) t) | C.Appl l -> C.Appl (List.map (aux n) l) | C.Const (uri,exp_named_subst) -> let exp_named_subst' = aux_exp_named_subst n exp_named_subst in @@ -159,15 +159,13 @@ let classify_metas newmeta in_subst_domain subst_in metasenv = match entry with Some (n,Cic.Decl s) -> Some (n,Cic.Decl (subst_in canonical_context' s)) - | Some (n,Cic.Def (s,None)) -> - Some (n,Cic.Def ((subst_in canonical_context' s),None)) | None -> None - | Some (n,Cic.Def (bo,Some ty)) -> + | Some (n,Cic.Def (bo,ty)) -> Some (n, Cic.Def (subst_in canonical_context' bo, - Some (subst_in canonical_context' ty))) + subst_in canonical_context' ty)) in entry'::canonical_context' ) canonical_context [] @@ -409,15 +407,8 @@ let cut_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst: CicMkImplicit.identity_relocation_list_for_metavariable context in let newmeta1ty = CicSubstitution.lift 1 ty in -(* This is the pre-letin implementation - let bo' = - C.Appl - [C.Lambda (fresh_name,term,C.Meta (newmeta1,irl1)) ; - C.Meta (newmeta2,irl2)] - in -*) let bo' = - Cic.LetIn (fresh_name, C.Meta (newmeta2,irl2), C.Meta (newmeta1,irl1)) + Cic.LetIn (fresh_name, C.Meta (newmeta2,irl2), term, C.Meta (newmeta1,irl1)) in let (newproof, _) = ProofEngineHelpers.subst_meta_in_proof proof metano bo' @@ -450,13 +441,13 @@ let letin_tac ?(mk_fresh_name_callback=FreshNamesGenerator.mk_fresh_name ~subst: let fresh_name = mk_fresh_name_callback metasenv context (Cic.Name "Hletin") ~typ:term in let context_for_newmeta = - (Some (fresh_name,C.Def (term,Some tty)))::context in + (Some (fresh_name,C.Def (term,tty)))::context in let irl = CicMkImplicit.identity_relocation_list_for_metavariable context_for_newmeta in let newmetaty = CicSubstitution.lift 1 ty in - let bo' = C.LetIn (fresh_name,term,C.Meta (newmeta,irl)) in + let bo' = C.LetIn (fresh_name,term,tty,C.Meta (newmeta,irl)) in let (newproof, _) = ProofEngineHelpers.subst_meta_in_proof proof metano bo'[newmeta,context_for_newmeta,newmetaty] @@ -602,9 +593,9 @@ let beta_after_elim_tac upto predicate = | C.Lambda (_, s, t) -> let s, t = gen_term k s, gen_term (succ k) t in if is_meta [s; t] then meta else C.Lambda (anon, s, t) - | C.LetIn (_, s, t) -> - let s, t = gen_term k s, gen_term (succ k) t in - if is_meta [s; t] then meta else C.LetIn (anon, s, t) + | C.LetIn (_, s, ty, t) -> + let s,ty,t = gen_term k s, gen_term k ty, gen_term (succ k) t in + if is_meta [s; t] then meta else C.LetIn (anon, s, ty, t) | C.Fix (i, fl) -> C.Fix (i, List.map (gen_fix (List.length fl) k) fl) | C.CoFix (i, fl) -> C.CoFix (i, List.map (gen_cofix (List.length fl) k) fl) in @@ -873,22 +864,3 @@ let elim_intros_simpl_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fres [ReductionTactics.simpl_tac ~pattern:(ProofEngineTypes.conclusion_pattern None)]) ;; - -(* FG: insetrts a "hole" in the context (derived from letin_tac) *) - -let letout_tac = - let mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[] in - let term = C.Sort C.Set in - let letout_tac (proof, goal) = - let curi, metasenv, _subst, pbo, pty, attrs = proof in - let metano, context, ty = CicUtil.lookup_meta goal metasenv in - let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in - let fresh_name = mk_fresh_name_callback metasenv context (Cic.Name "hole") ~typ:term in - let context_for_newmeta = None :: context in - let irl = CicMkImplicit.identity_relocation_list_for_metavariable context_for_newmeta in - let newmetaty = CicSubstitution.lift 1 ty in - let bo' = C.LetIn (fresh_name, term, C.Meta (newmeta,irl)) in - let newproof, _ = ProofEngineHelpers.subst_meta_in_proof proof metano bo'[newmeta,context_for_newmeta,newmetaty] in - newproof, [newmeta] - in - PET.mk_tactic letout_tac diff --git a/helm/software/components/tactics/primitiveTactics.mli b/helm/software/components/tactics/primitiveTactics.mli index 890874a89..492fbf601 100644 --- a/helm/software/components/tactics/primitiveTactics.mli +++ b/helm/software/components/tactics/primitiveTactics.mli @@ -88,10 +88,6 @@ val cases_intros_tac: (* FG *) -(* inserts a hole in the context *) -val letout_tac: - ProofEngineTypes.tactic - val mk_predicate_for_elim: context:Cic.context -> metasenv:Cic.metasenv -> ugraph:CicUniv.universe_graph -> goal:Cic.term -> diff --git a/helm/software/components/tactics/proofEngineHelpers.ml b/helm/software/components/tactics/proofEngineHelpers.ml index b38512273..7d223a443 100644 --- a/helm/software/components/tactics/proofEngineHelpers.ml +++ b/helm/software/components/tactics/proofEngineHelpers.ml @@ -48,10 +48,9 @@ let subst_meta_in_proof proof meta term newmetasenv = List.map (function Some (n,Cic.Decl s) -> Some (n,Cic.Decl (subst_in s)) - | Some (n,Cic.Def (s,None)) -> Some (n,Cic.Def (subst_in s,None)) | None -> None - | Some (n,Cic.Def (bo,Some ty)) -> - Some (n,Cic.Def (subst_in bo,Some (subst_in ty))) + | Some (n,Cic.Def (bo,ty)) -> + Some (n,Cic.Def (subst_in bo,subst_in ty)) ) canonical_context in i,canonical_context',(subst_in ty) @@ -95,10 +94,8 @@ let subst_meta_and_metasenv_in_proof proof meta subst newmetasenv = (function None -> None | Some (i,Cic.Decl t) -> Some (i,Cic.Decl (subst_in t)) - | Some (i,Cic.Def (t,None)) -> - Some (i,Cic.Def (subst_in t,None)) - | Some (i,Cic.Def (bo,Some ty)) -> - Some (i,Cic.Def (subst_in bo,Some (subst_in ty))) + | Some (i,Cic.Def (bo,ty)) -> + Some (i,Cic.Def (subst_in bo,subst_in ty)) ) canonical_context in (m,canonical_context',subst_in ty)::i @@ -151,14 +148,16 @@ let find_subterms ~subst ~metasenv ~ugraph ~wanted ~context t = (CicSubstitution.lift 1 w) t2 in subst,metasenv,ugraph,rest1 @ rest2 - | Cic.LetIn (name, t1, t2) -> + | Cic.LetIn (name, t1, t2, t3) -> let subst,metasenv,ugraph,rest1 = find subst metasenv ugraph context w t1 in let subst,metasenv,ugraph,rest2 = - find subst metasenv ugraph (Some (name, Cic.Def (t1,None))::context) - (CicSubstitution.lift 1 w) t2 + find subst metasenv ugraph context w t2 in + let subst,metasenv,ugraph,rest3 = + find subst metasenv ugraph (Some (name, Cic.Def (t1,t2))::context) + (CicSubstitution.lift 1 w) t3 in - subst,metasenv,ugraph,rest1 @ rest2 + subst,metasenv,ugraph,rest1 @ rest2 @ rest3 | Cic.Appl l -> List.fold_left (fun (subst,metasenv,ugraph,acc) t -> @@ -263,12 +262,16 @@ let select_in_term ~metasenv ~context ~ugraph ~term ~pattern:(wanted,where) = aux context s1 s2 @ aux (add_ctx context name (Cic.Decl s2)) t1 t2 | Cic.Prod (name1, s1, t1), Cic.Prod (name2, s2, t2) | Cic.Lambda (name1, s1, t1), Cic.Lambda (name2, s2, t2) -> [] - | Cic.LetIn (Cic.Anonymous, s1, t1), Cic.LetIn (name, s2, t2) -> - aux context s1 s2 @ aux (add_ctx context name (Cic.Def (s2,None))) t1 t2 - | Cic.LetIn (Cic.Name n1, s1, t1), - Cic.LetIn ((Cic.Name n2) as name, s2, t2) when n1 = n2-> - aux context s1 s2 @ aux (add_ctx context name (Cic.Def (s2,None))) t1 t2 - | Cic.LetIn (name1, s1, t1), Cic.LetIn (name2, s2, t2) -> [] + | Cic.LetIn (Cic.Anonymous, s1, ty1, t1), Cic.LetIn (name, s2, ty2, t2) -> + aux context s1 s2 @ + aux context ty1 ty2 @ + aux (add_ctx context name (Cic.Def (s2,ty2))) t1 t2 + | Cic.LetIn (Cic.Name n1, s1, ty1, t1), + Cic.LetIn ((Cic.Name n2) as name, s2, ty2, t2) when n1 = n2-> + aux context s1 s2 @ + aux context ty1 ty2 @ + aux (add_ctx context name (Cic.Def (s2,ty2))) t1 t2 + | Cic.LetIn (name1, s1, ty1, t1), Cic.LetIn (name2, s2, ty2, t2) -> [] | Cic.Appl terms1, Cic.Appl terms2 -> auxs context terms1 terms2 | Cic.Var (_, subst1), Cic.Var (_, subst2) | Cic.Const (_, subst1), Cic.Const (_, subst2) @@ -377,11 +380,12 @@ let pattern_of ?(equality=(==)) ~term terms = true, Cic.Lambda (Cic.Anonymous, s, t) else not_found - | Cic.LetIn (_, s, t) -> + | Cic.LetIn (_, s, ty, t) -> let b1,s = aux s in - let b2,t = aux t in - if b1||b2 then - true, Cic.LetIn (Cic.Anonymous, s, t) + let b2,ty = aux ty in + let b3,t = aux t in + if b1||b2||b3 then + true, Cic.LetIn (Cic.Anonymous, s, ty, t) else not_found | Cic.Appl terms -> @@ -525,7 +529,7 @@ exception Fail of string Lazy.t | Some (name,Cic.Def (bo, ty)) -> (match pattern with | None -> - let selected_ty=match ty with None -> None | Some _ -> Some [] in + let selected_ty = [] in subst,metasenv,ugraph,((Some (`Def ([],selected_ty)))::res), (entry::context) | Some pat -> @@ -533,14 +537,11 @@ exception Fail of string Lazy.t select_in_term ~metasenv ~context ~ugraph ~term:bo ~pattern:(what, Some pat) in let subst,metasenv,ugraph,terms_ty = - match ty with - None -> subst,metasenv,ugraph,None - | Some ty -> - let subst,metasenv,ugraph,res = - select_in_term ~metasenv ~context ~ugraph ~term:ty - ~pattern:(what, Some pat) - in - subst,metasenv,ugraph,Some res + let subst,metasenv,ugraph,res = + select_in_term ~metasenv ~context ~ugraph ~term:ty + ~pattern:(what, Some pat) + in + subst,metasenv,ugraph,res in subst,metasenv,ugraph,((Some (`Def (terms_bo,terms_ty)))::res), (entry::context)) @@ -575,8 +576,10 @@ let locate_in_term ?(equality=(fun _ -> (==))) what ~where context = | Cic.Prod (name, s, t) | Cic.Lambda (name, s, t) -> aux context s @ aux (add_ctx context name (Cic.Decl s)) t - | Cic.LetIn (name, s, t) -> - aux context s @ aux (add_ctx context name (Cic.Def (s,None))) t + | Cic.LetIn (name, s, ty, t) -> + aux context s @ + aux context ty @ + aux (add_ctx context name (Cic.Def (s,ty))) t | Cic.Appl tl -> auxs context tl | Cic.MutCase (_, _, out, t, pat) -> aux context out @ aux context t @ auxs context pat @@ -621,11 +624,7 @@ let locate_in_conjecture ?(equality=fun _ -> (==)) what (_,context,ty) = context',res | Some (_, Cic.Def (bo,ty)) -> let res = res @ locate_in_term what ~where:bo context in - let res = - match ty with - None -> res - | Some ty -> - res @ locate_in_term what ~where:ty context in + let res = res @ locate_in_term what ~where:ty context in let context' = entry::context in context',res ) context ([],[]) @@ -635,9 +634,7 @@ let locate_in_conjecture ?(equality=fun _ -> (==)) what (_,context,ty) = let lookup_type metasenv context hyp = let rec aux p = function | Some (Cic.Name name, Cic.Decl t) :: _ when name = hyp -> p, t - | Some (Cic.Name name, Cic.Def (_, Some t)) :: _ when name = hyp -> p, t - | Some (Cic.Name name, Cic.Def (u, _)) :: tail when name = hyp -> - p, fst (CicTypeChecker.type_of_aux' metasenv tail u CicUniv.empty_ugraph) + | Some (Cic.Name name, Cic.Def (_,t)) :: _ when name = hyp -> p, t | _ :: tail -> aux (succ p) tail | [] -> raise (ProofEngineTypes.Fail (lazy "lookup_type: not premise in the current goal")) in @@ -692,10 +689,9 @@ let relations_of_menv m c = (List.map (function | None -> [] - | Some (_,Cic.Decl t) - | Some (_,Cic.Def (t,None)) -> + | Some (_,Cic.Decl t) -> List.map fst (CicUtil.metas_of_term ty) - | Some (_,Cic.Def (t,Some ty)) -> + | Some (_,Cic.Def (t,ty)) -> List.map fst (CicUtil.metas_of_term ty) @ List.map fst (CicUtil.metas_of_term t)) ctx) diff --git a/helm/software/components/tactics/proofEngineHelpers.mli b/helm/software/components/tactics/proofEngineHelpers.mli index 39fb69b0d..a51213f93 100644 --- a/helm/software/components/tactics/proofEngineHelpers.mli +++ b/helm/software/components/tactics/proofEngineHelpers.mli @@ -79,7 +79,7 @@ val select: pattern:ProofEngineTypes.lazy_pattern -> Cic.substitution * Cic.metasenv * CicUniv.universe_graph * [ `Decl of (Cic.context * Cic.term) list - | `Def of (Cic.context * Cic.term) list * (Cic.context * Cic.term) list option + | `Def of (Cic.context * Cic.term) list * (Cic.context * Cic.term) list ] option list * (Cic.context * Cic.term) list diff --git a/helm/software/components/tactics/proofEngineReduction.ml b/helm/software/components/tactics/proofEngineReduction.ml index 68a2a0a3d..3892ace35 100644 --- a/helm/software/components/tactics/proofEngineReduction.ml +++ b/helm/software/components/tactics/proofEngineReduction.ml @@ -86,7 +86,7 @@ let replace ~equality ~what ~with_what ~where = | C.Cast (te,ty) -> C.Cast (aux te, aux ty) | C.Prod (n,s,t) -> C.Prod (n, aux s, aux t) | C.Lambda (n,s,t) -> C.Lambda (n, aux s, aux t) - | C.LetIn (n,s,t) -> C.LetIn (n, aux s, aux t) + | C.LetIn (n,s,ty,t) -> C.LetIn (n, aux s, aux ty, aux t) | C.Appl l -> (* Invariant enforced: no application of an application *) (match List.map aux l with @@ -139,7 +139,7 @@ let replace_lifting ~equality ~context ~what ~with_what ~where = find_image_aux (what,with_what) in let add_ctx ctx n s = (Some (n, Cic.Decl s))::ctx in - let add_ctx1 ctx n s = (Some (n, Cic.Def (s,None)))::ctx in + let add_ctx1 ctx n s ty = (Some (n, Cic.Def (s,ty)))::ctx in let rec substaux k ctx what t = try S.lift (k-1) (find_image ctx what t) @@ -169,9 +169,9 @@ let replace_lifting ~equality ~context ~what ~with_what ~where = | C.Lambda (n,s,t) -> C.Lambda (n, substaux k ctx what s, substaux (k + 1) (add_ctx ctx n s) (List.map (S.lift 1) what) t) - | C.LetIn (n,s,t) -> + | C.LetIn (n,s,ty,t) -> C.LetIn - (n, substaux k ctx what s, substaux (k + 1) (add_ctx1 ctx n s) (List.map (S.lift 1) what) t) + (n, substaux k ctx what s, substaux k ctx what ty, substaux (k + 1) (add_ctx1 ctx n s ty) (List.map (S.lift 1) what) t) | C.Appl (he::tl) -> (* Invariant: no Appl applied to another Appl *) let tl' = List.map (substaux k ctx what) tl in @@ -268,8 +268,8 @@ let replace_lifting_csc nnn ~equality ~what ~with_what ~where = C.Prod (n, substaux k s, substaux (k + 1) t) | C.Lambda (n,s,t) -> C.Lambda (n, substaux k s, substaux (k + 1) t) - | C.LetIn (n,s,t) -> - C.LetIn (n, substaux k s, substaux (k + 1) t) + | C.LetIn (n,s,ty,t) -> + C.LetIn (n, substaux k s, substaux k ty, substaux (k + 1) t) | C.Appl (he::tl) -> (* Invariant: no Appl applied to another Appl *) let tl' = List.map (substaux k) tl in @@ -358,8 +358,8 @@ let replace_with_rel_1_from ~equality ~what = C.Prod (n, subst_term k v, subst_term (succ k) t) | C.Lambda (n, v, t) -> C.Lambda (n, subst_term k v, subst_term (succ k) t) - | C.LetIn (n, v, t) -> - C.LetIn (n, subst_term k v, subst_term (succ k) t) + | C.LetIn (n, v, ty, t) -> + C.LetIn (n, subst_term k v, subst_term k ty, subst_term (succ k) t) | C.Fix (i, fixes) -> let fixesno = List.length fixes in let fixes = List.map (subst_fix fixesno k) fixes in @@ -543,7 +543,7 @@ let simpl context = | he::tl -> reduceaux context tl (S.subst he t) (* when name is Anonimous the substitution should be superfluous *) ) - | C.LetIn (n,s,t) -> + | C.LetIn (n,s,ty,t) -> reduceaux context l (S.subst (reduceaux context [] s) t) | C.Appl (he::tl) -> let tl' = List.map (reduceaux context []) tl in @@ -726,7 +726,7 @@ let simpl context = (* be superfluous *) aux (he::rev_constant_args) tl (S.subst he t) end - | C.LetIn (_,s,t) -> + | C.LetIn (_,s,_,t) -> aux rev_constant_args l (S.subst s t) | C.Fix (i,fl) -> let (_,recindex,_,body) = List.nth fl i in @@ -804,7 +804,7 @@ let simpl context = (* when name is Anonimous the substitution should *) (* be superfluous *) aux tl (S.subst he t)) - | C.LetIn (_,s,t) -> aux l (S.subst s t) + | C.LetIn (_,s,_,t) -> aux l (S.subst s t) | Cic.Appl (Cic.Const (uri,_) :: args) as t when is_fix uri -> let recno = prerr_endline ("cerco : " ^ string_of_int (guess_recno uri) diff --git a/helm/software/components/tactics/proofEngineStructuralRules.ml b/helm/software/components/tactics/proofEngineStructuralRules.ml index 755fab660..3f96677b8 100644 --- a/helm/software/components/tactics/proofEngineStructuralRules.ml +++ b/helm/software/components/tactics/proofEngineStructuralRules.ml @@ -46,21 +46,10 @@ let clearbody ~hyp = (fun entry context -> match entry with Some (C.Name hyp',C.Def (term,ty)) when hyp = hyp' -> - let cleared_entry = - let ty = - match ty with - Some ty -> ty - | None -> - fst - (CicTypeChecker.type_of_aux' metasenv context term - CicUniv.empty_ugraph) (* TASSI: FIXME *) - in - Some (C.Name hyp, Cic.Decl ty) - in + let cleared_entry = Some (C.Name hyp, Cic.Decl ty) in cleared_entry::context | None -> None::context - | Some (n,C.Decl t) - | Some (n,C.Def (t,None)) -> + | Some (n,C.Decl t) -> let _,_ = try CicTypeChecker.type_of_aux' metasenv context t @@ -75,7 +64,7 @@ let clearbody ~hyp = )) in entry::context - | Some (n,Cic.Def (te,Some ty)) -> + | Some (n,Cic.Def (te,ty)) -> (try ignore (CicTypeChecker.type_of_aux' metasenv context te @@ -136,8 +125,7 @@ let clear_one ~hyp = (true, None::context) | None -> (b, None::context) | Some (n,C.Decl t) - | Some (n,Cic.Def (t,Some _)) - | Some (n,C.Def (t,None)) -> + | Some (n,Cic.Def (t,_)) -> if b then let _,_ = try diff --git a/helm/software/components/tactics/reductionTactics.ml b/helm/software/components/tactics/reductionTactics.ml index e1bedeb20..8a0d739be 100644 --- a/helm/software/components/tactics/reductionTactics.ml +++ b/helm/software/components/tactics/reductionTactics.ml @@ -67,17 +67,9 @@ let reduction_tac ~reduction ~pattern (proof,goal) = Some (name,Cic.Decl ty')::context', metasenv, ugraph | Some (name,Cic.Def (bo,ty)),Some (`Def (selected_bo,selected_ty)) -> let bo', metasenv, ugraph = - change subst bo selected_bo metasenv ugraph - in + change subst bo selected_bo metasenv ugraph in let ty', metasenv, ugraph = - match ty,selected_ty with - None,None -> None, metasenv, ugraph - | Some ty,Some selected_ty -> - let ty', metasenv, ugraph = - change subst ty selected_ty metasenv ugraph - in - Some ty', metasenv, ugraph - | _,_ -> assert false + change subst ty selected_ty metasenv ugraph in (Some (name,Cic.Def (bo',ty'))::context'), metasenv, ugraph | _,_ -> assert false @@ -190,17 +182,9 @@ let change_tac ?(with_cast=false) ~pattern with_what = (Some (name,Cic.Decl ty')::context'), metasenv, ugraph | Some (name,Cic.Def (bo,ty)),Some (`Def (selected_bo,selected_ty)) -> let bo', metasenv, ugraph = - change subst bo selected_bo metasenv ugraph - in + change subst bo selected_bo metasenv ugraph in let ty', metasenv, ugraph = - match ty,selected_ty with - None,None -> None, metasenv, ugraph - | Some ty,Some selected_ty -> - let ty', metasenv, ugraph = - change subst ty selected_ty metasenv ugraph - in - Some ty', metasenv, ugraph - | _,_ -> assert false + change subst ty selected_ty metasenv ugraph in (Some (name,Cic.Def (bo',ty'))::context'), metasenv, ugraph | _,_ -> assert false diff --git a/helm/software/components/tactics/setoids.ml b/helm/software/components/tactics/setoids.ml index 7d0e958cc..c8ca16317 100644 --- a/helm/software/components/tactics/setoids.ml +++ b/helm/software/components/tactics/setoids.ml @@ -1745,7 +1745,7 @@ let relation_rewrite_in id c1 c2 (direction,eqclause) ~new_goals gl = let hyp = CicSubstitution.subst (CicSubstitution.lift 1 c2) hyp in (* Since CicSubstitution.subst has killed Rel 1 and decreased the other Rels, Rel 1 is now coding for c2, we can build the let-in factorizing c2 *) - Cic.LetIn (Cic.Anonymous,c2,hyp) + Cic.LetIn (Cic.Anonymous,c2,assert false,hyp) in let new_hyp = (*COQ Termops.replace_term c1 c2 hyp*) assert false in let oppdir = opposite_direction direction in diff --git a/helm/software/components/tactics/universe.ml b/helm/software/components/tactics/universe.ml index 99041ed1b..6a0a31566 100644 --- a/helm/software/components/tactics/universe.ml +++ b/helm/software/components/tactics/universe.ml @@ -85,10 +85,11 @@ let rec dummies_of_coercions = let s' = dummies_of_coercions s in let t' = dummies_of_coercions t in Cic.Prod (n,s',t') - | Cic.LetIn(n,s,t) -> + | Cic.LetIn(n,s,ty,t) -> let s' = dummies_of_coercions s in + let ty' = dummies_of_coercions ty in let t' = dummies_of_coercions t in - Cic.LetIn (n,s',t') + Cic.LetIn (n,s',ty',t') | Cic.MutCase _ -> Cic.Meta (-1,[]) | t -> t ;; diff --git a/helm/software/components/tactics/variousTactics.ml b/helm/software/components/tactics/variousTactics.ml index 3a3db7db4..5563f206b 100644 --- a/helm/software/components/tactics/variousTactics.ml +++ b/helm/software/components/tactics/variousTactics.ml @@ -46,15 +46,9 @@ let assumption_tac = (Some (_, C.Decl t)) when fst (R.are_convertible context (S.lift n t) ty CicUniv.empty_ugraph) -> n - | (Some (_, C.Def (_,Some ty'))) when + | (Some (_, C.Def (_,ty'))) when fst (R.are_convertible context (S.lift n ty') ty CicUniv.empty_ugraph) -> n - | (Some (_, C.Def (t,None))) -> - let ty_t, u = (* TASSI: FIXME *) - CicTypeChecker.type_of_aux' metasenv context (S.lift n t) - CicUniv.empty_ugraph in - let b,_ = R.are_convertible context ty_t ty u in - if b then n else find (n+1) tl | _ -> find (n+1) tl ) | [] -> raise (PET.Fail (lazy "Assumption: No such assumption")) diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml index 477e775d8..ae33d1f83 100644 --- a/helm/software/matita/matitaScript.ml +++ b/helm/software/matita/matitaScript.ml @@ -241,9 +241,9 @@ let cic2grafite context menv t = | Cic.Prod (Cic.Name n, s, t) -> PT.Binder (`Forall, (PT.Ident (n,None), Some (aux c s)), aux (Some (Cic.Name n, Cic.Decl s)::c) t) - | Cic.LetIn (Cic.Name n, s, t) -> + | Cic.LetIn (Cic.Name n, s, ty, t) -> PT.Binder (`Lambda, (PT.Ident (n,None), Some (aux c s)), - aux (Some (Cic.Name n, Cic.Def (s,None))::c) t) + aux (Some (Cic.Name n, Cic.Def (s,ty))::c) t) | Cic.Meta _ -> PT.Implicit | Cic.Sort (Cic.Type u) -> PT.Sort (`Type u) | Cic.Sort Cic.Set -> PT.Sort `Set -- 2.39.2