From 265cf771fbfe217b5f274b999fc3ad887683a09a Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 5 Sep 2003 10:29:13 +0000 Subject: [PATCH] Defs in context may now have an optional type (when unknown). During type-checking, LetIn are pushed in the context as Defs with a known type. When a Rel pointing to a Def in the context is found, the already computed type (if present) is used instead of re-typing the body of the LetIn. As a result, we get a (possibly exponential) decrease in the complexity of the typing algorithm. --- helm/ocaml/cic/cic.ml | 5 +- helm/ocaml/cic/deannotate.ml | 2 +- helm/ocaml/cic_omdoc/cic2acic.ml | 126 ++++++++---- helm/ocaml/cic_omdoc/eta_fixing.ml | 23 +-- helm/ocaml/cic_proof_checking/cicPp.ml | 23 +-- .../cic_proof_checking/cicReductionMachine.ml | 11 +- .../cic_proof_checking/cicReductionNaif.ml | 11 +- .../cic_proof_checking/cicTypeChecker.ml | 55 ++++-- helm/ocaml/cic_transformations/sequentPp.ml | 6 +- helm/ocaml/cic_unification/cicRefine.ml | 15 +- helm/ocaml/cic_unification/cicUnification.ml | 186 +++++++++--------- helm/ocaml/tactics/fourierR.ml | 6 +- helm/ocaml/tactics/primitiveTactics.ml | 12 +- helm/ocaml/tactics/proofEngineHelpers.ml | 7 +- helm/ocaml/tactics/proofEngineReduction.ml | 4 +- .../tactics/proofEngineStructuralRules.ml | 9 +- helm/ocaml/tactics/reductionTactics.ml | 8 +- helm/ocaml/tactics/variousTactics.ml | 4 +- 18 files changed, 300 insertions(+), 213 deletions(-) diff --git a/helm/ocaml/cic/cic.ml b/helm/ocaml/cic/cic.ml index fd46c22b4..6d58e6164 100644 --- a/helm/ocaml/cic/cic.ml +++ b/helm/ocaml/cic/cic.ml @@ -171,7 +171,7 @@ and annotation = and context_entry = (* A declaration or definition *) Decl of term - | Def of term + | Def of term * term option (* body, type (if known) *) and hypothesis = (name * context_entry) option (* None means no more accessible *) @@ -185,4 +185,5 @@ and anncontext_entry = (* A declaration or definition *) and annhypothesis = id * (name * anncontext_entry) option (* None means no more accessible *) -and anncontext = annhypothesis list;; +and anncontext = annhypothesis list +;; diff --git a/helm/ocaml/cic/deannotate.ml b/helm/ocaml/cic/deannotate.ml index df59305fe..2bee18d6f 100644 --- a/helm/ocaml/cic/deannotate.ml +++ b/helm/ocaml/cic/deannotate.ml @@ -108,7 +108,7 @@ let deannotate_obj = List.map (function _,Some (n,(C.ADef at)) -> - Some (n,(C.Def (deannotate_term at))) + Some (n,(C.Def ((deannotate_term at),None))) | _,Some (n,(C.ADecl at)) -> Some (n,(C.Decl (deannotate_term at))) | _,None -> None diff --git a/helm/ocaml/cic_omdoc/cic2acic.ml b/helm/ocaml/cic_omdoc/cic2acic.ml index c0e514d37..4226364fc 100644 --- a/helm/ocaml/cic_omdoc/cic2acic.ml +++ b/helm/ocaml/cic_omdoc/cic2acic.ml @@ -23,6 +23,26 @@ * http://cs.unibo.it/helm/. *) +let hashtbl_add_time = ref 0.0;; + +let xxx_add h k v = + let t1 = Sys.time () in + Hashtbl.add h k v ; + let t2 = Sys.time () in + hashtbl_add_time := !hashtbl_add_time +. t2 -. t1 +;; + +let number_new_type_of_aux' = ref 0;; +let type_of_aux'_add_time = ref 0.0;; + +let xxx_type_of_aux' m c t = + let t1 = Sys.time () in + let res = TypeInference.type_of_aux' m c t in + let t2 = Sys.time () in + type_of_aux'_add_time := !type_of_aux'_add_time +. t2 -. t1 ; + res +;; + type anntypes = {annsynthesized : Cic.annterm ; annexpected : Cic.annterm option} ;; @@ -36,8 +56,8 @@ let gen_id seed = let fresh_id seed ids_to_terms ids_to_father_ids = fun father t -> let res = gen_id seed in - Hashtbl.add ids_to_father_ids res father ; - Hashtbl.add ids_to_terms res t ; + xxx_add ids_to_father_ids res father ; + xxx_add ids_to_terms res t ; res ;; @@ -60,14 +80,15 @@ let acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts ids_to_inner_types metasenv context idrefs t expectedty = let module D = DoubleTypeInference in - let module T = CicTypeChecker in let module C = Cic in let fresh_id' = fresh_id seed ids_to_terms ids_to_father_ids in -prerr_endline "*************** INIZIO DOUBLE TYPE INFERENCE ************"; + let time1 = Sys.time () in let terms_to_types = D.double_type_of metasenv context t expectedty in -prerr_endline "*************** FINE DOUBLE TYPE INFERENCE ************"; + let time2 = Sys.time () in + prerr_endline + ("++++++++++++ Tempi della double_type_of: "^ string_of_float (time2 -. time1)) ; let rec aux computeinnertypes father context idrefs tt = let fresh_id'' = fresh_id' father tt in (*CSC: computeinnertypes era true, il che e' proprio sbagliato, no? *) @@ -90,6 +111,10 @@ prerr_endline "*************** FINE DOUBLE TYPE INFERENCE ************"; (*CSC: type-inference, but the result is very poor. As a very weak *) (*CSC: patch, I apply whd to the computed type. Full beta *) (*CSC: reduction would be a much better option. *) +(*CSC: solo per testare i tempi *) +(*XXXXXXX *) + try +(* *) let {D.synthesized = synthesized; D.expected = expected} = if computeinnertypes then D.CicHash.find terms_to_types tt @@ -97,10 +122,13 @@ prerr_endline "*************** FINE DOUBLE TYPE INFERENCE ************"; (* We are already in an inner-type and Coscoy's double *) (* type inference algorithm has not been applied. *) {D.synthesized = - CicReduction.whd context (T.type_of_aux' metasenv context tt) ; +(***CSC: patch per provare i tempi + CicReduction.whd context (xxx_type_of_aux' metasenv context tt) ; *) +Cic.Sort Cic.Type ; D.expected = None} in - let innersort = T.type_of_aux' metasenv context synthesized in + incr number_new_type_of_aux' ; + let innersort = (*XXXXX *) xxx_type_of_aux' metasenv context synthesized (* Cic.Sort Cic.Prop *) in let ainnertypes,expected_available = if computeinnertypes then let annexpected,expected_available = @@ -120,11 +148,17 @@ prerr_endline "*************** FINE DOUBLE TYPE INFERENCE ************"; None,false in ainnertypes,synthesized, string_of_sort innersort, expected_available +(*XXXXXXXX *) + with + Not_found -> (* l'inner-type non e' nella tabella ==> sort <> Prop *) + (* CSC: Type or Set? I can not tell *) + None,Cic.Sort Cic.Type,"Type",false +(* *) in let add_inner_type id = match ainnertypes with None -> () - | Some ainnertypes -> Hashtbl.add ids_to_inner_types id ainnertypes + | Some ainnertypes -> xxx_add ids_to_inner_types id ainnertypes in match tt with C.Rel n -> @@ -133,12 +167,12 @@ prerr_endline "*************** FINE DOUBLE TYPE INFERENCE ************"; (Some (C.Name s,_)) -> s | _ -> raise NameExpected in - Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; + xxx_add ids_to_inner_sorts fresh_id'' innersort ; if innersort = "Prop" && expected_available then add_inner_type fresh_id'' ; C.ARel (fresh_id'', List.nth idrefs (n-1), n, id) | C.Var (uri,exp_named_subst) -> - Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; + xxx_add ids_to_inner_sorts fresh_id'' innersort ; if innersort = "Prop" && expected_available then add_inner_type fresh_id'' ; let exp_named_subst' = @@ -150,7 +184,7 @@ prerr_endline "*************** FINE DOUBLE TYPE INFERENCE ************"; let (_,canonical_context,_) = List.find (function (m,_,_) -> n = m) metasenv in - Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; + xxx_add ids_to_inner_sorts fresh_id'' innersort ; if innersort = "Prop" && expected_available then add_inner_type fresh_id'' ; C.AMeta (fresh_id'', n, @@ -164,21 +198,21 @@ prerr_endline "*************** FINE DOUBLE TYPE INFERENCE ************"; | C.Sort s -> C.ASort (fresh_id'', s) | C.Implicit -> C.AImplicit (fresh_id'') | C.Cast (v,t) -> - Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; + xxx_add ids_to_inner_sorts fresh_id'' innersort ; if innersort = "Prop" then add_inner_type fresh_id'' ; C.ACast (fresh_id'', aux' context idrefs v, aux' context idrefs t) | C.Prod (n,s,t) -> - Hashtbl.add ids_to_inner_sorts fresh_id'' + xxx_add ids_to_inner_sorts fresh_id'' (string_of_sort innertype) ; - let sourcetype = T.type_of_aux' metasenv context s in - Hashtbl.add ids_to_inner_sorts (source_id_of_id fresh_id'') + let sourcetype = xxx_type_of_aux' metasenv context s in + xxx_add ids_to_inner_sorts (source_id_of_id fresh_id'') (string_of_sort sourcetype) ; let n' = match n with C.Anonymous -> n | C.Name n' -> - if D.does_not_occur 1 t then + if TypeInference.does_not_occur 1 t then C.Anonymous else C.Name n' @@ -187,9 +221,9 @@ prerr_endline "*************** FINE DOUBLE TYPE INFERENCE ************"; (fresh_id'', n', aux' context idrefs s, aux' ((Some (n, C.Decl s))::context) (fresh_id''::idrefs) t) | C.Lambda (n,s,t) -> - Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; - let sourcetype = T.type_of_aux' metasenv context s in - Hashtbl.add ids_to_inner_sorts (source_id_of_id fresh_id'') + xxx_add ids_to_inner_sorts fresh_id'' innersort ; + let sourcetype = xxx_type_of_aux' metasenv context s in + xxx_add ids_to_inner_sorts (source_id_of_id fresh_id'') (string_of_sort sourcetype) ; if innersort = "Prop" then begin @@ -208,19 +242,19 @@ prerr_endline "*************** FINE DOUBLE TYPE INFERENCE ************"; (fresh_id'',n, aux' context idrefs s, aux' ((Some (n, C.Decl s)::context)) (fresh_id''::idrefs) t) | C.LetIn (n,s,t) -> - Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; + 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))::context) (fresh_id''::idrefs) t) + aux' ((Some (n, C.Def(s,None)))::context) (fresh_id''::idrefs) t) | C.Appl l -> - Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; + xxx_add ids_to_inner_sorts fresh_id'' innersort ; if innersort = "Prop" then add_inner_type fresh_id'' ; C.AAppl (fresh_id'', List.map (aux' context idrefs) l) | C.Const (uri,exp_named_subst) -> - Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; + xxx_add ids_to_inner_sorts fresh_id'' innersort ; if innersort = "Prop" && expected_available then add_inner_type fresh_id'' ; let exp_named_subst' = @@ -235,7 +269,7 @@ prerr_endline "*************** FINE DOUBLE TYPE INFERENCE ************"; in C.AMutInd (fresh_id'', uri, tyno, exp_named_subst') | C.MutConstruct (uri,tyno,consno,exp_named_subst) -> - Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; + xxx_add ids_to_inner_sorts fresh_id'' innersort ; if innersort = "Prop" && expected_available then add_inner_type fresh_id'' ; let exp_named_subst' = @@ -244,7 +278,7 @@ prerr_endline "*************** FINE DOUBLE TYPE INFERENCE ************"; in C.AMutConstruct (fresh_id'', uri, tyno, consno, exp_named_subst') | C.MutCase (uri, tyno, outty, term, patterns) -> - Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; + xxx_add ids_to_inner_sorts fresh_id'' innersort ; if innersort = "Prop" then add_inner_type fresh_id'' ; C.AMutCase (fresh_id'', uri, tyno, aux' context idrefs outty, @@ -256,7 +290,7 @@ prerr_endline "*************** FINE DOUBLE TYPE INFERENCE ************"; let tys = List.map (fun (name,_,ty,_) -> Some (C.Name name, C.Decl ty)) funs in - Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; + xxx_add ids_to_inner_sorts fresh_id'' innersort ; if innersort = "Prop" then add_inner_type fresh_id'' ; C.AFix (fresh_id'', funno, @@ -273,7 +307,7 @@ prerr_endline "*************** FINE DOUBLE TYPE INFERENCE ************"; let tys = List.map (fun (name,ty,_) -> Some (C.Name name, C.Decl ty)) funs in - Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; + xxx_add ids_to_inner_sorts fresh_id'' innersort ; if innersort = "Prop" then add_inner_type fresh_id'' ; C.ACoFix (fresh_id'', funno, @@ -284,7 +318,12 @@ prerr_endline "*************** FINE DOUBLE TYPE INFERENCE ************"; ) fresh_idrefs funs ) in - aux true None context idrefs t + let timea = Sys.time () in + let res = aux true None context idrefs t in + let timeb = Sys.time () in + prerr_endline + ("+++++++++++++ Tempi della aux dentro alla acic_of_cic: "^ string_of_float (timeb -. timea)) ; + res ;; let acic_of_cic_context metasenv context idrefs t = @@ -341,7 +380,6 @@ let acic_object_of_cic_object obj = C.AVariable ("mettereaposto",id,abo,aty, params) | C.CurrentProof (id,conjectures,bo,ty,params) -> -prerr_endline "************* INIZIO ETA_FIXING (congetture) ********" ; let conjectures' = List.map (function (i,canonical_context,term) -> @@ -350,19 +388,20 @@ prerr_endline "************* INIZIO ETA_FIXING (congetture) ********" ; (function None -> None | Some (n, C.Decl t)-> Some (n, C.Decl (E.eta_fix conjectures t)) - | Some (n, C.Def t) -> Some (n, C.Def (E.eta_fix conjectures t)) + | Some (n, C.Def (t,None)) -> + Some (n, C.Def ((E.eta_fix conjectures t),None)) + | Some (_,C.Def (_,Some _)) -> assert false ) canonical_context in let term' = E.eta_fix conjectures term in (i,canonical_context',term') ) conjectures in -prerr_endline "************* INIZIO CIC ==> ACIC (congetture) ********" ; let aconjectures = List.map (function (i,canonical_context,term) as conjecture -> let cid = "c" ^ string_of_int !conjectures_seed in - Hashtbl.add ids_to_conjectures cid conjecture ; + xxx_add ids_to_conjectures cid conjecture ; incr conjectures_seed ; let idrefs',revacanonical_context = let rec aux context idrefs = @@ -371,7 +410,7 @@ prerr_endline "************* INIZIO CIC ==> ACIC (congetture) ********" ; | hyp::tl -> let hid = "h" ^ string_of_int !hypotheses_seed in let new_idrefs = hid::idrefs in - Hashtbl.add ids_to_hypotheses hid hyp ; + xxx_add ids_to_hypotheses hid hyp ; incr hypotheses_seed ; match hyp with (Some (n,C.Decl t)) -> @@ -382,7 +421,7 @@ prerr_endline "************* INIZIO CIC ==> ACIC (congetture) ********" ; conjectures context idrefs t None in final_idrefs,(hid,Some (n,C.ADecl at))::atl - | (Some (n,C.Def t)) -> + | (Some (n,C.Def (t,_))) -> let final_idrefs,atl = aux (hyp::context) new_idrefs tl in let at = @@ -404,13 +443,28 @@ prerr_endline "************* INIZIO CIC ==> ACIC (congetture) ********" ; in (cid,i,(List.rev revacanonical_context),aterm) ) conjectures' in -prerr_endline "*********** INIZIO ETA FIXING PROVA **********"; + let time1 = Sys.time () in let bo' = E.eta_fix conjectures' bo in let ty' = E.eta_fix conjectures' ty in -prerr_endline "*********** INIZIO CIC ==> ACIC PROVA **********"; + let time2 = Sys.time () in + prerr_endline + ("++++++++++ Tempi della eta_fix: "^ string_of_float (time2 -. time1)) ; + hashtbl_add_time := 0.0 ; + type_of_aux'_add_time := 0.0 ; let abo = acic_term_of_cic_term_context' conjectures' [] [] bo' (Some ty') in let aty = acic_term_of_cic_term_context' conjectures' [] [] ty' None in + let time3 = Sys.time () in + prerr_endline + ("++++++++++++ Tempi della hashtbl_add_time: " ^ string_of_float !hashtbl_add_time) ; + prerr_endline + ("++++++++++++ Tempi della type_of_aux'_add_time(" ^ string_of_int !number_new_type_of_aux' ^ "): " ^ string_of_float !type_of_aux'_add_time) ; + prerr_endline + ("++++++++++++ Tempi della type_of_aux'_add_time nella double_type_inference(" ^ string_of_int !DoubleTypeInference.number_new_type_of_aux'_double_work ^ ";" ^ string_of_int !DoubleTypeInference.number_new_type_of_aux'_prop ^ "/" ^ string_of_int !DoubleTypeInference.number_new_type_of_aux' ^ "): " ^ string_of_float !DoubleTypeInference.type_of_aux'_add_time) ; + prerr_endline + ("++++++++++ Tempi della acic_of_cic: " ^ string_of_float (time3 -. time2)) ; + prerr_endline + ("++++++++++ Numero di iterazioni della acic_of_cic: " ^ string_of_int !seed) ; C.ACurrentProof ("mettereaposto","mettereaposto2",id,aconjectures,abo,aty,params) | C.InductiveDefinition (tys,params,paramsno) -> diff --git a/helm/ocaml/cic_omdoc/eta_fixing.ml b/helm/ocaml/cic_omdoc/eta_fixing.ml index 876c5c678..81668203d 100644 --- a/helm/ocaml/cic_omdoc/eta_fixing.ml +++ b/helm/ocaml/cic_omdoc/eta_fixing.ml @@ -27,6 +27,8 @@ exception ReferenceToVariable;; exception RferenceToCurrentProof;; exception ReferenceToInductiveDefinition;; +let prerr_endline _ = ();; + (* let rec fix_lambdas_wrt_type ty te = let module C = Cic in @@ -163,8 +165,8 @@ let fix_according_to_type ty hd tl = let eta_fix metasenv t = let rec eta_fix' context t = - prerr_endline ("entering aux with: term=" ^ CicPp.ppterm t); - flush stderr ; + (* prerr_endline ("entering aux with: term=" ^ CicPp.ppterm t); + flush stderr ; *) let module C = Cic in let module S = CicSubstitution in match t with @@ -200,7 +202,7 @@ let eta_fix metasenv t = (n, eta_fix' context s, eta_fix' ((Some (n,(C.Decl s)))::context) t) | C.LetIn (n,s,t) -> C.LetIn - (n, eta_fix' context s, eta_fix' ((Some (n,(C.Def s)))::context) t) + (n,eta_fix' context s,eta_fix' ((Some (n,(C.Def (s,None))))::context) t) | C.Appl l as appl -> let l' = List.map (eta_fix' context) l in @@ -214,11 +216,7 @@ let eta_fix metasenv t = | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition ) in - let result = fix_according_to_type constant_type (C.Const(uri,exp_named_subst)) l'' in - if not (CicReduction.are_convertible [] appl result) then - (prerr_endline ("prima :" ^(CicPp.ppterm appl)); - prerr_endline ("dopo :" ^(CicPp.ppterm result))); - result + fix_according_to_type constant_type (C.Const(uri,exp_named_subst)) l'' | _ -> C.Appl l' ) | C.Const (uri,exp_named_subst) -> let exp_named_subst' = @@ -263,7 +261,7 @@ let eta_fix metasenv t = List.map (fun (_,t) -> t) constructors else let term_type = - CicTypeChecker.type_of_aux' metasenv context term in + TypeInference.type_of_aux' metasenv context term in (match term_type with C.Appl (hd::params) -> List.map (fun (_,t) -> clean_up t params) constructors @@ -271,12 +269,7 @@ let eta_fix metasenv t = let patterns2 = List.map2 fix_lambdas_wrt_type constructor_types patterns in - let dopo = - C.MutCase (uri, tyno, outty',term',patterns2) in - if not (CicReduction.are_convertible [] prima dopo) then - (prerr_endline ("prima :" ^(CicPp.ppterm prima)); - prerr_endline ("dopo :" ^(CicPp.ppterm dopo))); - dopo + C.MutCase (uri, tyno, outty',term',patterns2) | C.Fix (funno, funs) -> let fun_types = List.map (fun (n,_,ty,_) -> Some (C.Name n,(Cic.Decl ty))) funs in diff --git a/helm/ocaml/cic_proof_checking/cicPp.ml b/helm/ocaml/cic_proof_checking/cicPp.ml index d3f7f0f60..11ed4418c 100644 --- a/helm/ocaml/cic_proof_checking/cicPp.ml +++ b/helm/ocaml/cic_proof_checking/cicPp.ml @@ -220,20 +220,21 @@ let ppobj obj = List.fold_right (fun (n, context, t) i -> let conjectures',name_context = - List.fold_right - (fun context_entry (i,name_context) -> - (match context_entry with - Some (n,C.Decl at) -> + List.fold_right + (fun context_entry (i,name_context) -> + (match context_entry with + Some (n,C.Decl at) -> (separate i) ^ - string_of_name n ^ ":" ^ pp at name_context ^ " ", - (Some n)::name_context - | Some (n,C.Def at) -> + string_of_name n ^ ":" ^ pp at name_context ^ " ", + (Some n)::name_context + | Some (n,C.Def (at,None)) -> (separate i) ^ - string_of_name n ^ ":= " ^ pp at name_context ^ " ", - (Some n)::name_context + string_of_name n ^ ":= " ^ pp at name_context ^ " ", + (Some n)::name_context | None -> - (separate i) ^ "_ :? _ ", None::name_context) - ) context ("",[]) + (separate i) ^ "_ :? _ ", None::name_context + | _ -> assert false) + ) context ("",[]) in conjectures' ^ " |- " ^ "?" ^ (string_of_int n) ^ ": " ^ pp t name_context ^ "\n" ^ i diff --git a/helm/ocaml/cic_proof_checking/cicReductionMachine.ml b/helm/ocaml/cic_proof_checking/cicReductionMachine.ml index 30b688264..61e7aaaef 100644 --- a/helm/ocaml/cic_proof_checking/cicReductionMachine.ml +++ b/helm/ocaml/cic_proof_checking/cicReductionMachine.ml @@ -515,7 +515,7 @@ if List.mem uri params then prerr_endline "---- OK2" ; match List.nth context (n - 1 - k) with None -> assert false | Some (_,C.Decl _) -> None - | Some (_,C.Def x) -> Some (S.lift (n - k) x) + | Some (_,C.Def (x,_)) -> Some (S.lift (n - k) x) end with _ -> None @@ -805,11 +805,14 @@ let are_convertible = ) true l1 l2 | (C.Sort s1, C.Sort s2) -> true (*CSC da finire con gli universi *) | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) -> - aux context s1 s2 && aux ((Some (name1, (C.Decl s1)))::context) t1 t2 + aux context s1 s2 && + aux ((Some (name1, (C.Decl s1)))::context) t1 t2 | (C.Lambda (name1,s1,t1), C.Lambda(_,s2,t2)) -> - aux context s1 s2 && aux ((Some (name1, (C.Decl s1)))::context) t1 t2 + aux context s1 s2 && + aux ((Some (name1, (C.Decl s1)))::context) t1 t2 | (C.LetIn (name1,s1,t1), C.LetIn(_,s2,t2)) -> - aux context s1 s2 && aux ((Some (name1, (C.Def s1)))::context) t1 t2 + aux context s1 s2 && + aux ((Some (name1, (C.Def (s1,None))))::context) t1 t2 | (C.Appl l1, C.Appl l2) -> (try List.fold_right2 (fun x y b -> aux context x y && b) l1 l2 true diff --git a/helm/ocaml/cic_proof_checking/cicReductionNaif.ml b/helm/ocaml/cic_proof_checking/cicReductionNaif.ml index 987f4b6ed..5dce7c68d 100644 --- a/helm/ocaml/cic_proof_checking/cicReductionNaif.ml +++ b/helm/ocaml/cic_proof_checking/cicReductionNaif.ml @@ -53,7 +53,7 @@ let whd context = C.Rel n as t -> (match List.nth context (n-1) with Some (_, C.Decl _) -> if l = [] then t else C.Appl (t::l) - | Some (_, C.Def bo) -> whdaux l (S.lift n bo) + | Some (_, C.Def (bo,_)) -> whdaux l (S.lift n bo) | None -> raise RelToHiddenHypothesis ) | C.Var (uri,exp_named_subst) as t -> @@ -217,11 +217,14 @@ let are_convertible = ) true l1 l2 | (C.Sort s1, C.Sort s2) -> true (*CSC da finire con gli universi *) | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) -> - aux context s1 s2 && aux ((Some (name1, (C.Decl s1)))::context) t1 t2 + aux context s1 s2 && + aux ((Some (name1, (C.Decl s1)))::context) t1 t2 | (C.Lambda (name1,s1,t1), C.Lambda(_,s2,t2)) -> - aux context s1 s2 && aux ((Some (name1, (C.Decl s1)))::context) t1 t2 + aux context s1 s2 && + aux ((Some (name1, (C.Decl s1)))::context) t1 t2 | (C.LetIn (name1,s1,t1), C.LetIn(_,s2,t2)) -> - aux context s1 s2 && aux ((Some (name1, (C.Def s1)))::context) t1 t2 + aux context s1 s2 && + aux ((Some (name1, (C.Def (s1,None))))::context) t1 t2 | (C.Appl l1, C.Appl l2) -> (try List.fold_right2 (fun x y b -> aux context x y && b) l1 l2 true diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml index 48d8b2ea9..62dc951aa 100644 --- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml +++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml @@ -217,13 +217,16 @@ and does_not_occur context n nn te = does_not_occur context n nn te && does_not_occur context n nn ty | C.Prod (name,so,dest) -> does_not_occur context n nn so && - does_not_occur((Some (name,(C.Decl so)))::context) (n + 1) (nn + 1) dest + does_not_occur((Some (name,(C.Decl so)))::context) (n + 1) (nn + 1) + dest | C.Lambda (name,so,dest) -> does_not_occur context n nn so && - does_not_occur((Some (name,(C.Decl so)))::context) (n + 1) (nn + 1) dest + does_not_occur((Some (name,(C.Decl so)))::context) (n + 1) (nn + 1) + dest | C.LetIn (name,so,dest) -> does_not_occur context n nn so && - does_not_occur ((Some (name,(C.Def so)))::context) (n + 1) (nn + 1) dest + does_not_occur ((Some (name,(C.Def (so,None))))::context) + (n + 1) (nn + 1) dest | C.Appl l -> List.fold_right (fun x i -> i && does_not_occur context n nn x) l true | C.Var (_,exp_named_subst) @@ -403,7 +406,8 @@ and strictly_positive context n nn te = (fun x i -> i && weakly_positive - ((Some (C.Name name,(Cic.Decl ity)))::context) (n+1) (nn+1) uri x + ((Some (C.Name name,(Cic.Decl ity)))::context) (n+1) (nn+1) uri + x ) cl' true | t -> does_not_occur context n nn t @@ -672,7 +676,7 @@ and check_is_really_smaller_arg context n nn kl x safes te = (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta | C.LetIn (name,so,ta) -> check_is_really_smaller_arg context n nn kl x safes so && - check_is_really_smaller_arg ((Some (name,(C.Def so)))::context) + check_is_really_smaller_arg ((Some (name,(C.Def (so,None))))::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 *) @@ -689,7 +693,8 @@ and check_is_really_smaller_arg context n nn kl x safes te = match CicEnvironment.get_obj uri with C.InductiveDefinition (tl,_,paramsno) -> let tys = - List.map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) tl + List.map + (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) tl in let (_,isinductive,_,cl) = List.nth tl i in let cl' = @@ -727,7 +732,8 @@ and check_is_really_smaller_arg context n nn kl x safes te = C.InductiveDefinition (tl,_,paramsno) -> let (_,isinductive,_,cl) = List.nth tl i in let tys = - List.map (fun (n,_,ty,_) -> Some(Cic.Name n,(Cic.Decl ty))) tl + List.map (fun (n,_,ty,_) -> + Some(Cic.Name n,(Cic.Decl ty))) tl in let cl' = List.map @@ -801,7 +807,8 @@ and guarded_by_destructors context n nn kl x safes = | C.Rel n -> (match List.nth context (n-1) with Some (_,C.Decl _) -> true - | Some (_,C.Def bo) -> guarded_by_destructors context n nn kl x safes bo + | Some (_,C.Def (bo,_)) -> + guarded_by_destructors context n nn kl x safes bo | None -> raise (TypeCheckerFailure RelToHiddenHypothesis) ) | C.Meta _ @@ -820,7 +827,7 @@ and guarded_by_destructors context n nn kl x safes = (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta | C.LetIn (name,so,ta) -> guarded_by_destructors context n nn kl x safes so && - guarded_by_destructors ((Some (name,(C.Def so)))::context) + guarded_by_destructors ((Some (name,(C.Def (so,None))))::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 @@ -850,7 +857,8 @@ and guarded_by_destructors context n nn kl x safes = C.InductiveDefinition (tl,_,paramsno) -> let (_,isinductive,_,cl) = List.nth tl i in let tys = - List.map (fun (n,_,ty,_) -> Some(Cic.Name n,(Cic.Decl ty))) tl + List.map (fun (n,_,ty,_) -> + Some(Cic.Name n,(Cic.Decl ty))) tl in let cl' = List.map @@ -892,7 +900,8 @@ and guarded_by_destructors context n nn kl x safes = C.InductiveDefinition (tl,_,paramsno) -> let (_,isinductive,_,cl) = List.nth tl i in let tys = - List.map (fun (n,_,ty,_) -> Some(Cic.Name n,(Cic.Decl ty))) tl + List.map + (fun (n,_,ty,_) -> Some(Cic.Name n,(Cic.Decl ty))) tl in let cl' = List.map @@ -1058,8 +1067,8 @@ and guarded_by_constructors context n nn h te args coInductiveTypeURI = [] -> true | he::tl -> analyse_branch context so he && - analyse_instantiated_type ((Some (name,(C.Decl so)))::context) - de tl + analyse_instantiated_type + ((Some (name,(C.Decl so)))::context) de tl end | C.Lambda _ | C.LetIn _ -> @@ -1147,7 +1156,7 @@ and guarded_by_constructors context n nn h te args coInductiveTypeURI = let n_plus_len = n + len and nn_plus_len = nn + len (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *) - and tys = List.map (fun (n,_,ty,_) -> Some (C.Name n,(C.Decl ty))) fl in + and tys = List.map (fun (n,_,ty,_)-> Some (C.Name n,(C.Decl ty))) fl in List.fold_right (fun (_,_,ty,bo) i -> i && does_not_occur context n nn ty && @@ -1293,9 +1302,10 @@ and check_metasenv_consistency metasenv context canonical_context l = [] -> [] | (Some (n,C.Decl t))::tl -> (Some (n,C.Decl (S.lift_meta l (S.lift i t))))::(aux (i+1) tl) - | (Some (n,C.Def t))::tl -> - (Some (n,C.Def (S.lift_meta l (S.lift i t))))::(aux (i+1) tl) + | (Some (n,C.Def (t,None)))::tl -> + (Some (n,C.Def ((S.lift_meta l (S.lift i t)),None)))::(aux (i+1) tl) | None::tl -> None::(aux (i+1) tl) + | (Some (n,C.Def (_,Some _)))::_ -> assert false in aux 1 canonical_context in @@ -1304,7 +1314,7 @@ and check_metasenv_consistency metasenv context canonical_context l = let res = match (t,ct) with _,None -> true - | Some t,Some (_,C.Def ct) -> + | Some t,Some (_,C.Def (ct,_)) -> R.are_convertible context t ct | Some t,Some (_,C.Decl ct) -> R.are_convertible context (type_of_aux' metasenv context t) ct @@ -1325,8 +1335,11 @@ and type_of_aux' metasenv context t = (try match List.nth context (n - 1) with Some (_,C.Decl t) -> S.lift n t - | Some (_,C.Def bo) -> type_of_aux context (S.lift n bo) - | None -> raise (TypeCheckerFailure RelToHiddenHypothesis) + | Some (_,C.Def (_,Some ty)) -> S.lift n ty + | Some (_,C.Def (bo,None)) -> + prerr_endline "##### CASO DA INVESTIGARE E CAPIRE" ; + type_of_aux context (S.lift n bo) + | None -> raise (TypeCheckerFailure RelToHiddenHypothesis) with _ -> raise (TypeCheckerFailure (NotWellTyped "Not a close term")) ) @@ -1363,7 +1376,7 @@ and type_of_aux' metasenv context t = C.Prod (n,s,type2) | C.LetIn (n,s,t) -> (* only to check if s is well-typed *) - let _ = type_of_aux context s in + let ty = type_of_aux context s in (* 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)) @@ -1377,7 +1390,7 @@ and type_of_aux' metasenv context t = (* One-step LetIn reduction. Even faster than the previous solution. Moreover the inferred type is closer to the expected one. *) (CicSubstitution.subst s - (type_of_aux ((Some (n,(C.Def s)))::context) t)) + (type_of_aux ((Some (n,(C.Def (s,Some ty))))::context) t)) | C.Appl (he::tl) when List.length tl > 0 -> let hetype = type_of_aux context he and tlbody_and_type = List.map (fun x -> (x, type_of_aux context x)) tl in diff --git a/helm/ocaml/cic_transformations/sequentPp.ml b/helm/ocaml/cic_transformations/sequentPp.ml index bda66841c..e7b3151ea 100644 --- a/helm/ocaml/cic_transformations/sequentPp.ml +++ b/helm/ocaml/cic_transformations/sequentPp.ml @@ -38,10 +38,11 @@ module TextualPp = match i with Some (n,Cic.Decl t) -> print_name n ^ ":" ^ CicPp.pp t context ^ "\n", (Some n)::context - | Some (n,Cic.Def t) -> + | Some (n,Cic.Def (t,None)) -> print_name n ^ ":=" ^ CicPp.pp t context ^ "\n", (Some n)::context | None -> "_ ?= _\n", None::context + | Some (_,Cic.Def (_,Some _)) -> assert false in output^newoutput,context' ) ctx ("",[]) @@ -84,7 +85,7 @@ module XmlPp = Hashtbl.add ids_to_hypotheses hid binding ; incr hypotheses_seed ; match binding with - (Some (n,(Cic.Def t as b)) as entry) + (Some (n,(Cic.Def (t,None) as b)) as entry) | (Some (n,(Cic.Decl t as b)) as entry) -> let acic = acic_of_cic_context context idrefs t None in [< s ; @@ -97,6 +98,7 @@ module XmlPp = | None -> (* Invariant: "" is never looked up *) [< s ; X.xml_empty "Hidden" [] >], (None::context), ""::idrefs + | Some (_,Cic.Def (_,Some _)) -> assert false ) context ([<>],[],[]) ) in diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml index e5e846982..881c72bfd 100644 --- a/helm/ocaml/cic_unification/cicRefine.ml +++ b/helm/ocaml/cic_unification/cicRefine.ml @@ -96,7 +96,9 @@ and type_of_aux' metasenv context t = (try match List.nth context (n - 1) with Some (_,C.Decl t) -> S.lift n t,subst,metasenv - | Some (_,C.Def bo) -> + | Some (_,C.Def (_,Some ty)) -> S.lift n ty,subst,metasenv + | Some (_,C.Def (bo,None)) -> + prerr_endline "##### DA INVESTIGARE E CAPIRE" ; type_of_aux subst metasenv context (S.lift n bo) | None -> raise RelToHiddenHypothesis with @@ -160,9 +162,9 @@ and type_of_aux' metasenv context t = C.Prod (n,s,type2),subst'''',metasenv'''' | C.LetIn (n,s,t) -> (* only to check if s is well-typed *) - let _,subst',metasenv' = type_of_aux subst metasenv context s in + let ty,subst',metasenv' = type_of_aux subst metasenv context s in let inferredty,subst'',metasenv'' = - type_of_aux subst' metasenv' ((Some (n,(C.Def s)))::context) t + type_of_aux subst' metasenv' ((Some (n,(C.Def (s,Some ty))))::context) t in (* One-step LetIn reduction. Even faster than the previous solution. Moreover the inferred type is closer to the expected one. *) @@ -224,9 +226,10 @@ and type_of_aux' metasenv context t = [] -> [] | (Some (n,C.Decl t))::tl -> (Some (n,C.Decl (S.lift_meta l (S.lift i t))))::(aux (i+1) tl) - | (Some (n,C.Def t))::tl -> - (Some (n,C.Def (S.lift_meta l (S.lift i t))))::(aux (i+1) tl) + | (Some (n,C.Def (t,None)))::tl -> + (Some (n,C.Def ((S.lift_meta l (S.lift i t)),None)))::(aux (i+1) tl) | None::tl -> None::(aux (i+1) tl) + | (Some (_,C.Def (_,Some _)))::_ -> assert false in aux 1 canonical_context in @@ -234,7 +237,7 @@ and type_of_aux' metasenv context t = (fun (subst,metasenv) t ct -> match (t,ct) with _,None -> subst,metasenv - | Some t,Some (_,C.Def ct) -> + | Some t,Some (_,C.Def (ct,_)) -> (try CicUnification.fo_unif_subst subst context metasenv t ct with _ -> raise MetasenvInconsistency) diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml index f7c19073b..306074ec9 100644 --- a/helm/ocaml/cic_unification/cicUnification.ml +++ b/helm/ocaml/cic_unification/cicUnification.ml @@ -49,14 +49,14 @@ let position n = let restrict to_be_restricted = let rec erase i n = function - [] -> [] - | _::tl when List.mem (n,i) to_be_restricted -> - None::(erase (i+1) n tl) + [] -> [] + | _::tl when List.mem (n,i) to_be_restricted -> + None::(erase (i+1) n tl) | he::tl -> he::(erase (i+1) n tl) in let rec aux = function - [] -> [] - | (n,context,t)::tl -> (n,erase 1 n context,t)::(aux tl) in + [] -> [] + | (n,context,t)::tl -> (n,erase 1 n context,t)::(aux tl) in aux ;; @@ -72,13 +72,13 @@ let delift context metasenv l t = C.Rel m (*CSC: che succede se c'e' un Def? Dovrebbe averlo gia' *) (*CSC: deliftato la regola per il LetIn *) else - (match List.nth context (m-k-1) with - Some (_,C.Def t) -> deliftaux k (S.lift m t) - | Some (_,C.Decl t) -> + (match List.nth context (m-k-1) with + Some (_,C.Def (t,_)) -> deliftaux k (S.lift m t) + | Some (_,C.Decl t) -> (* It may augment to_be_restricted *) ignore (deliftaux k (S.lift m t)) ; C.Rel ((position (m-k) l) + k) - | None -> raise RelToHiddenHypothesis) + | None -> raise RelToHiddenHypothesis) | C.Var (uri,exp_named_subst) -> let exp_named_subst' = List.map (function (uri,t) -> uri,deliftaux k t) exp_named_subst @@ -177,7 +177,7 @@ let rec fo_unif_subst subst context metasenv t1 t2 = (* First possibility: restriction *) (* Second possibility: unification *) (* Third possibility: convertibility *) - R.are_convertible context t1' t2' + R.are_convertible context t1' t2' ) true ln lm in if ok then subst,metasenv else raise UnificationFailed @@ -186,18 +186,18 @@ let rec fo_unif_subst subst context metasenv t1 t2 = | (C.Meta (n,l), t) | (t, C.Meta (n,l)) -> let subst',metasenv' = - try - let oldt = (List.assoc n subst) in - let lifted_oldt = S.lift_meta l oldt in - fo_unif_subst subst context metasenv lifted_oldt t - with Not_found -> - let t',metasenv' = delift context metasenv l t in - (n, t')::subst, metasenv' + try + let oldt = (List.assoc n subst) in + let lifted_oldt = S.lift_meta l oldt in + fo_unif_subst subst context metasenv lifted_oldt t + with Not_found -> + let t',metasenv' = delift context metasenv l t in + (n, t')::subst, metasenv' in - let (_,_,meta_type) = - List.find (function (m,_,_) -> m=n) metasenv' in - let tyt = CicTypeChecker.type_of_aux' metasenv' context t in - fo_unif_subst subst' context metasenv' (S.lift_meta l meta_type) tyt + let (_,_,meta_type) = + List.find (function (m,_,_) -> m=n) metasenv' in + let tyt = CicTypeChecker.type_of_aux' metasenv' context t in + fo_unif_subst subst' context metasenv' (S.lift_meta l meta_type) tyt | (C.Var (uri1,exp_named_subst1),C.Var (uri2,exp_named_subst2)) | (C.Const (uri1,exp_named_subst1),C.Const (uri2,exp_named_subst2)) -> if UriManager.eq uri1 uri2 then @@ -259,7 +259,7 @@ let rec fo_unif_subst subst context metasenv t1 t2 = in fo_unif_l subst' metasenv' (l1,l2) in - fo_unif_l subst metasenv (lr1, lr2) + fo_unif_l subst metasenv (lr1, lr2) | (C.Const _, _) | (_, C.Const _) | (C.MutInd _, _) @@ -274,9 +274,9 @@ let rec fo_unif_subst subst context metasenv t1 t2 = let subst', metasenv' = fo_unif_subst subst context metasenv outt1 outt2 in let subst'',metasenv'' = - fo_unif_subst subst' context metasenv' t1 t2 in + fo_unif_subst subst' context metasenv' t1 t2 in List.fold_left2 - (function (subst,metasenv) -> + (function (subst,metasenv) -> fo_unif_subst subst context metasenv ) (subst'',metasenv'') pl1 pl2 | (C.Fix _, _) @@ -322,24 +322,24 @@ in canonical_context. *) let restrict canonical_context m k l = let rec erase i = function - [] -> [] - | None::tl -> None::(erase (i+1) tl) - | he::tl -> - let i' = (List.nth l (i-1)) in - if i' <= k - then he::(erase (i+1) tl) (* local variable *) - else - let acc = - (try List.nth canonical_context (i'-k-1) - with Failure _ -> None) in - if acc = None - then None::(erase (i+1) tl) - else he::(erase (i+1) tl) in + [] -> [] + | None::tl -> None::(erase (i+1) tl) + | he::tl -> + let i' = (List.nth l (i-1)) in + if i' <= k + then he::(erase (i+1) tl) (* local variable *) + else + let acc = + (try List.nth canonical_context (i'-k-1) + with Failure _ -> None) in + if acc = None + then None::(erase (i+1) tl) + else he::(erase (i+1) tl) in let rec aux = function - [] -> [] - | (n,context,t)::tl when n=m -> (n,erase 1 context,t)::tl - | hd::tl -> hd::(aux tl) + [] -> [] + | (n,context,t)::tl when n=m -> (n,erase 1 context,t)::tl + | hd::tl -> hd::(aux tl) in aux ;; @@ -378,39 +378,39 @@ CSCSCS | C.Sort _ -> metasenv | C.Implicit -> metasenv | C.Cast (te,ty) -> - let metasenv' = aux metasenv k te in - aux metasenv' k ty + let metasenv' = aux metasenv k te in + aux metasenv' k ty | C.Prod (_,s,t) | C.Lambda (_,s,t) | C.LetIn (_,s,t) -> - let metasenv' = aux metasenv k s in - aux metasenv' (k+1) t + let metasenv' = aux metasenv k s in + aux metasenv' (k+1) t | C.Appl l -> - List.fold_left - (function metasenv -> aux metasenv k) metasenv l + List.fold_left + (function metasenv -> aux metasenv k) metasenv l | C.Const _ | C.MutInd _ | C.MutConstruct _ -> metasenv | C.MutCase (_,_,_,outty,t,pl) -> - let metasenv' = aux metasenv k outty in - let metasenv'' = aux metasenv' k t in - List.fold_left - (function metasenv -> aux metasenv k) metasenv'' pl + let metasenv' = aux metasenv k outty in + let metasenv'' = aux metasenv' k t in + List.fold_left + (function metasenv -> aux metasenv k) metasenv'' pl | C.Fix (i, fl) -> let len = List.length fl in List.fold_left (fun metasenv f -> - let (_,_,ty,bo) = f in - let metasenv' = aux metasenv k ty in - aux metasenv' (k+len) bo + let (_,_,ty,bo) = f in + let metasenv' = aux metasenv k ty in + aux metasenv' (k+len) bo ) metasenv fl | C.CoFix (i, fl) -> - let len = List.length fl in + let len = List.length fl in List.fold_left (fun metasenv f -> - let (_,ty,bo) = f in - let metasenv' = aux metasenv k ty in - aux metasenv' (k+len) bo + let (_,ty,bo) = f in + let metasenv' = aux metasenv k ty in + aux metasenv' (k+len) bo ) metasenv fl in aux metasenv 0 ;; @@ -427,18 +427,18 @@ let unwind metasenv subst unwinded t = C.Rel _ as t -> t,metasenv | C.Var _ as t -> t,metasenv | C.Meta (i,l) -> - (try + (try S.lift_meta l (List.assoc i !unwinded), metasenv with Not_found -> if List.mem i !frozen then raise OccurCheck else let saved_frozen = !frozen in - frozen := i::!frozen ; + frozen := i::!frozen ; let res = try - let t = List.assoc i subst in + let t = List.assoc i subst in let t',metasenv' = um_aux metasenv t in - let _,metasenv'' = + let _,metasenv'' = let (_,canonical_context,_) = List.find (function (m,_,_) -> m=i) metasenv in @@ -451,13 +451,13 @@ let unwind metasenv subst unwinded t = (* not constrained variable, i.e. free in subst*) let l',metasenv' = List.fold_right - (fun t (tl,metasenv) -> + (fun t (tl,metasenv) -> match t with None -> None::tl,metasenv | Some t -> - let t',metasenv' = um_aux metasenv t in - (Some t')::tl, metasenv' - ) l ([],metasenv) + let t',metasenv' = um_aux metasenv t in + (Some t')::tl, metasenv' + ) l ([],metasenv) in C.Meta (i,l'), metasenv' in @@ -485,10 +485,10 @@ let unwind metasenv subst unwinded t = | C.Appl (he::tl) -> let tl',metasenv' = List.fold_right - (fun t (tl,metasenv) -> - let t',metasenv' = um_aux metasenv t in - t'::tl, metasenv' - ) tl ([],metasenv) + (fun t (tl,metasenv) -> + let t',metasenv' = um_aux metasenv t in + t'::tl, metasenv' + ) tl ([],metasenv) in begin match um_aux metasenv' he with @@ -499,28 +499,28 @@ let unwind metasenv subst unwinded t = | C.Const (uri,exp_named_subst) -> let exp_named_subst', metasenv' = List.fold_right - (fun (uri,t) (tl,metasenv) -> - let t',metasenv' = um_aux metasenv t in - (uri,t')::tl, metasenv' - ) exp_named_subst ([],metasenv) + (fun (uri,t) (tl,metasenv) -> + let t',metasenv' = um_aux metasenv t in + (uri,t')::tl, metasenv' + ) exp_named_subst ([],metasenv) in C.Const (uri,exp_named_subst'),metasenv' | C.MutInd (uri,typeno,exp_named_subst) -> let exp_named_subst', metasenv' = List.fold_right - (fun (uri,t) (tl,metasenv) -> - let t',metasenv' = um_aux metasenv t in - (uri,t')::tl, metasenv' - ) exp_named_subst ([],metasenv) + (fun (uri,t) (tl,metasenv) -> + let t',metasenv' = um_aux metasenv t in + (uri,t')::tl, metasenv' + ) exp_named_subst ([],metasenv) in C.MutInd (uri,typeno,exp_named_subst'),metasenv' | C.MutConstruct (uri,typeno,consno,exp_named_subst) -> let exp_named_subst', metasenv' = List.fold_right - (fun (uri,t) (tl,metasenv) -> - let t',metasenv' = um_aux metasenv t in - (uri,t')::tl, metasenv' - ) exp_named_subst ([],metasenv) + (fun (uri,t) (tl,metasenv) -> + let t',metasenv' = um_aux metasenv t in + (uri,t')::tl, metasenv' + ) exp_named_subst ([],metasenv) in C.MutConstruct (uri,typeno,consno,exp_named_subst'),metasenv' | C.MutCase (sp,i,outty,t,pl) -> @@ -528,10 +528,10 @@ let unwind metasenv subst unwinded t = let t',metasenv'' = um_aux metasenv' t in let pl',metasenv''' = List.fold_right - (fun p (pl,metasenv) -> - let p',metasenv' = um_aux metasenv p in - p'::pl, metasenv' - ) pl ([],metasenv'') + (fun p (pl,metasenv) -> + let p',metasenv' = um_aux metasenv p in + p'::pl, metasenv' + ) pl ([],metasenv'') in C.MutCase (sp, i, outty', t', pl'),metasenv''' | C.Fix (i, fl) -> @@ -539,10 +539,10 @@ let unwind metasenv subst unwinded t = let liftedfl,metasenv' = List.fold_right (fun (name, i, ty, bo) (fl,metasenv) -> - let ty',metasenv' = um_aux metasenv ty in - let bo',metasenv'' = um_aux metasenv' bo in - (name, i, ty', bo')::fl,metasenv'' - ) fl ([],metasenv) + let ty',metasenv' = um_aux metasenv ty in + let bo',metasenv'' = um_aux metasenv' bo in + (name, i, ty', bo')::fl,metasenv'' + ) fl ([],metasenv) in C.Fix (i, liftedfl),metasenv' | C.CoFix (i, fl) -> @@ -550,10 +550,10 @@ let unwind metasenv subst unwinded t = let liftedfl,metasenv' = List.fold_right (fun (name, ty, bo) (fl,metasenv) -> - let ty',metasenv' = um_aux metasenv ty in - let bo',metasenv'' = um_aux metasenv' bo in - (name, ty', bo')::fl,metasenv'' - ) fl ([],metasenv) + let ty',metasenv' = um_aux metasenv ty in + let bo',metasenv'' = um_aux metasenv' bo in + (name, ty', bo')::fl,metasenv'' + ) fl ([],metasenv) in C.CoFix (i, liftedfl),metasenv' in diff --git a/helm/ocaml/tactics/fourierR.ml b/helm/ocaml/tactics/fourierR.ml index b1aa1a256..a807554c5 100644 --- a/helm/ocaml/tactics/fourierR.ml +++ b/helm/ocaml/tactics/fourierR.ml @@ -886,8 +886,10 @@ 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))::next -> [Some(name,Cic.Def( - 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(( + CicSubstitution.lift n a),Some (CicSubstitution.lift n ty)))] @ superlift next (n+1) | _::next -> superlift next (n+1) (*?? ??*) ;; diff --git a/helm/ocaml/tactics/primitiveTactics.ml b/helm/ocaml/tactics/primitiveTactics.ml index 91cd6198e..8dfdd66c4 100644 --- a/helm/ocaml/tactics/primitiveTactics.ml +++ b/helm/ocaml/tactics/primitiveTactics.ml @@ -50,7 +50,7 @@ let lambda_abstract context newmeta ty mk_fresh_name = (context',ty,C.Lambda(n',s,bo)) | C.LetIn (n,s,t) -> let (context',ty,bo) = - collect_context ((Some (n,(C.Def s)))::context) t + collect_context ((Some (n,(C.Def (s,None))))::context) t in (context',ty,C.LetIn(n,s,bo)) | _ as t -> @@ -132,9 +132,10 @@ 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) -> - Some (n,Cic.Def (subst_in canonical_context' s)) + | Some (n,Cic.Def (s,None)) -> + Some (n,Cic.Def ((subst_in canonical_context' s),None)) | None -> None + | Some (_,Cic.Def (_,Some _)) -> assert false in entry'::canonical_context' ) canonical_context [] @@ -361,7 +362,7 @@ let letin_tac let fresh_name = mk_fresh_name_callback context (Cic.Name "Hletin") ~typ:term in let context_for_newmeta = - (Some (fresh_name,C.Def term))::context in + (Some (fresh_name,C.Def (term,None)))::context in let irl = identity_relocation_list_for_metavariable context_for_newmeta in let newmetaty = CicSubstitution.lift 1 ty in @@ -547,9 +548,10 @@ let change_tac ~what ~with_what ~status:(proof, goal) = let context' = List.map (function - Some (name,Cic.Def t) -> Some (name,Cic.Def (replace t)) + Some (name,Cic.Def (t,None)) -> Some (name,Cic.Def ((replace t),None)) | Some (name,Cic.Decl t) -> Some (name,Cic.Decl (replace t)) | None -> None + | Some (_,Cic.Def (_,Some _)) -> assert false ) context in let metasenv' = diff --git a/helm/ocaml/tactics/proofEngineHelpers.ml b/helm/ocaml/tactics/proofEngineHelpers.ml index 16be77edb..ac5850ca2 100644 --- a/helm/ocaml/tactics/proofEngineHelpers.ml +++ b/helm/ocaml/tactics/proofEngineHelpers.ml @@ -100,8 +100,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) -> Some (n,Cic.Def (subst_in s)) + | Some (n,Cic.Def (s,None)) -> Some (n,Cic.Def ((subst_in s),None)) | None -> None + | Some (_,Cic.Def (_,Some _)) -> assert false ) canonical_context in i,canonical_context',(subst_in ty) @@ -136,7 +137,9 @@ let subst_meta_and_metasenv_in_proof proof meta subst_in newmetasenv = (function None -> None | Some (i,Cic.Decl t) -> Some (i,Cic.Decl (subst_in t)) - | Some (i,Cic.Def t) -> Some (i,Cic.Def (subst_in t)) + | Some (i,Cic.Def (t,None)) -> + Some (i,Cic.Def ((subst_in t),None)) + | Some (_,Cic.Def (_,Some _)) -> assert false ) canonical_context in (m,canonical_context',subst_in ty)::i diff --git a/helm/ocaml/tactics/proofEngineReduction.ml b/helm/ocaml/tactics/proofEngineReduction.ml index c70be1fb7..9e5aa04ff 100644 --- a/helm/ocaml/tactics/proofEngineReduction.ml +++ b/helm/ocaml/tactics/proofEngineReduction.ml @@ -382,7 +382,7 @@ let reduce context = C.Rel n as t -> (match List.nth context (n-1) with Some (_,C.Decl _) -> if l = [] then t else C.Appl (t::l) - | Some (_,C.Def bo) -> reduceaux context l (S.lift n bo) + | Some (_,C.Def (bo,_)) -> reduceaux context l (S.lift n bo) | None -> raise RelToHiddenHypothesis ) | C.Var (uri,exp_named_subst) -> @@ -604,7 +604,7 @@ let simpl context = C.Rel n as t -> (match List.nth context (n-1) with Some (_,C.Decl _) -> if l = [] then t else C.Appl (t::l) - | Some (_,C.Def bo) -> + | Some (_,C.Def (bo,_)) -> try_delta_expansion l t (S.lift n bo) | None -> raise RelToHiddenHypothesis ) diff --git a/helm/ocaml/tactics/proofEngineStructuralRules.ml b/helm/ocaml/tactics/proofEngineStructuralRules.ml index d89420f58..07ddf3a9e 100644 --- a/helm/ocaml/tactics/proofEngineStructuralRules.ml +++ b/helm/ocaml/tactics/proofEngineStructuralRules.ml @@ -29,8 +29,9 @@ let clearbody ~hyp ~status:(proof, goal) = let module C = Cic in match hyp with None -> assert false + | Some (_, C.Def (_, Some _)) -> assert false | Some (_, C.Decl _) -> raise (Fail "No Body To Clear") - | Some (n_to_clear_body, C.Def term) as hyp_to_clear_body -> + | Some (n_to_clear_body, C.Def (term,None)) as hyp_to_clear_body -> let curi,metasenv,pbo,pty = proof in let metano,_,_ = List.find (function (m,_,_) -> m=goal) metasenv in let string_of_name = @@ -56,7 +57,7 @@ let clearbody ~hyp ~status:(proof, goal) = cleared_entry::context | None -> None::context | Some (n,C.Decl t) - | Some (n,C.Def t) -> + | Some (n,C.Def (t,None)) -> let _ = try CicTypeChecker.type_of_aux' metasenv context t @@ -71,6 +72,7 @@ let clearbody ~hyp ~status:(proof, goal) = ) in entry::context + | Some (_,Cic.Def (_,Some _)) -> assert false ) canonical_context [] in let _ = @@ -113,8 +115,9 @@ let clear ~hyp:hyp_to_clear ~status:(proof, goal) = match entry with t when t == hyp_to_clear -> None::context | None -> None::context + | Some (_,Cic.Def (_,Some _)) -> assert false | Some (n,C.Decl t) - | Some (n,C.Def t) -> + | Some (n,C.Def (t,None)) -> let _ = try CicTypeChecker.type_of_aux' metasenv context t diff --git a/helm/ocaml/tactics/reductionTactics.ml b/helm/ocaml/tactics/reductionTactics.ml index b29873a1f..55eacc234 100644 --- a/helm/ocaml/tactics/reductionTactics.ml +++ b/helm/ocaml/tactics/reductionTactics.ml @@ -69,11 +69,12 @@ let reduction_tac ~also_in_hypotheses ~reduction ~terms ~status:(proof,goal) = List.fold_right (fun entry context -> match entry with - Some (name,Cic.Def t) -> - (Some (name,Cic.Def (replace context t)))::context + Some (name,Cic.Def (t,None)) -> + (Some (name,Cic.Def ((replace context t),None)))::context | Some (name,Cic.Decl t) -> (Some (name,Cic.Decl (replace context t)))::context | None -> None::context + | Some (_,Cic.Def (_,Some _)) -> assert false ) context [] else context @@ -110,8 +111,9 @@ let fold_tac ~reduction ~also_in_hypotheses ~term ~status:(proof,goal) = List.map (function Some (n,Cic.Decl t) -> Some (n,Cic.Decl (replace t)) - | Some (n,Cic.Def t) -> Some (n,Cic.Def (replace t)) + | Some (n,Cic.Def (t,None)) -> Some (n,Cic.Def ((replace t),None)) | None -> None + | Some (_,Cic.Def (_,Some _)) -> assert false ) context else context diff --git a/helm/ocaml/tactics/variousTactics.ml b/helm/ocaml/tactics/variousTactics.ml index 390d97fb7..395768db9 100644 --- a/helm/ocaml/tactics/variousTactics.ml +++ b/helm/ocaml/tactics/variousTactics.ml @@ -39,7 +39,9 @@ let assumption_tac ~status:((proof,goal) as status) = (match hd with (Some (_, C.Decl t)) when (R.are_convertible context (S.lift n t) ty) -> n - | (Some (_, C.Def t)) when + | (Some (_, C.Def (_,Some ty'))) when + (R.are_convertible context ty' ty) -> n + | (Some (_, C.Def (t,None))) when (R.are_convertible context (CicTypeChecker.type_of_aux' metasenv context (S.lift n t)) ty) -> n | _ -> find (n+1) tl -- 2.39.2