From d344d41028275b6d1451dca8e40a88e33e588389 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Sat, 3 May 2008 21:31:45 +0000 Subject: [PATCH] Bug fixed in handling of explicit named substitutions: it could happen that explicit named substitution are merged not in the expected order. This happens comparing the case of an instantiation inside and outside a (nested) section. Thus I have added back the re-ordering of the explicit named substitution in CicSubstitution.subst_vars and in CicReduction.unwind_aux. Moreover, I have added to CicTypechecker.type_of_aux' the check that verifies if an explicit named substitution is ordered. --- .../cic_proof_checking/cicReduction.ml | 54 ++++++------------ .../cic_proof_checking/cicSubstitution.ml | 56 +++++++++++-------- .../cic_proof_checking/cicTypeChecker.ml | 33 ++++++++--- helm/software/components/ng_kernel/TEST | 8 +-- 4 files changed, 78 insertions(+), 73 deletions(-) diff --git a/helm/software/components/cic_proof_checking/cicReduction.ml b/helm/software/components/cic_proof_checking/cicReduction.ml index 11fd51235..5e02fdbaa 100644 --- a/helm/software/components/cic_proof_checking/cicReduction.ml +++ b/helm/software/components/cic_proof_checking/cicReduction.ml @@ -523,31 +523,7 @@ debug_print (lazy ("%%%%%UWVAR " ^ String.concat " ; " (List.map (function (uri, in C.CoFix (i, substitutedfl) and substaux_in_exp_named_subst params exp_named_subst' m = - (*CSC: Idea di Andrea di ordinare compatibilmente con l'ordine dei params - let ens' = - List.map (function (uri,t) -> uri, unwind_aux m t) exp_named_subst' @ - (*CSC: qui liftiamo tutti gli ens anche se magari me ne servono la meta'!!! *) - List.map (function (uri,t) -> uri, CicSubstitution.lift m t) ens - in - let rec filter_and_lift = - function - [] -> [] - | uri::tl -> - let r = filter_and_lift tl in - (try - (uri,(List.assq uri ens'))::r - with - Not_found -> r - ) - in - filter_and_lift params - *) - - (*CSC: invece di concatenare sarebbe meglio rispettare l'ordine dei params *) - (*CSC: e' vero???? una veloce prova non sembra confermare la teoria *) - - (*CSC: codice copiato e modificato dalla cicSubstitution.subst_vars *) - (*CSC: codice altamente inefficiente *) + (*CSC: codice copiato e modificato dalla cicSubstitution.subst_vars *) let rec filter_and_lift already_instantiated = function [] -> [] @@ -562,18 +538,24 @@ debug_print (lazy ("%%%%%UWVAR " ^ String.concat " ; " (List.map (function (uri, (uri,CicSubstitution.lift m (RS.from_ens_for_unwind ~unwind t)) :: (filter_and_lift (uri::already_instantiated) tl) | _::tl -> filter_and_lift already_instantiated tl -(* - | (uri,_)::tl -> -debug_print (lazy ("---- SKIPPO " ^ UriManager.string_of_uri uri)) ; -if List.for_all (function (uri',_) -> not (UriManager.eq uri uri')) -exp_named_subst' then debug_print (lazy "---- OK1") ; -debug_print (lazy ("++++ uri " ^ UriManager.string_of_uri uri ^ " not in " ^ String.concat " ; " (List.map UriManager.string_of_uri params))) ; -if List.mem uri params then debug_print (lazy "---- OK2") ; - filter_and_lift tl -*) in - List.map (function (uri,t) -> uri, unwind_aux m t) exp_named_subst' @ - (filter_and_lift [] (List.rev ens)) + let res = + List.map (function (uri,t) -> uri, unwind_aux m t) exp_named_subst' @ + (filter_and_lift [] (List.rev ens)) + in + let rec reorder = + function + [] -> [] + | uri::tl -> + let he = + try + [uri,List.assoc uri res] + with + Not_found -> [] + in + he@reorder tl + in + reorder params in unwind_aux m t diff --git a/helm/software/components/cic_proof_checking/cicSubstitution.ml b/helm/software/components/cic_proof_checking/cicSubstitution.ml index 8d1dad9e2..ba2c8f723 100644 --- a/helm/software/components/cic_proof_checking/cicSubstitution.ml +++ b/helm/software/components/cic_proof_checking/cicSubstitution.ml @@ -32,7 +32,13 @@ exception ReferenceToConstant;; exception ReferenceToCurrentProof;; exception ReferenceToInductiveDefinition;; -let debug_print = fun _ -> () +let debug = false +let debug_print = + if debug then + fun m -> prerr_endline (Lazy.force m) + else + fun _ -> () +;; let lift_from k n = let rec liftaux k = @@ -230,19 +236,9 @@ debug_print (lazy ("@@@POSSIBLE BUG: SUBSTITUTION IS NOT SIMULTANEOUS")) ; | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition ) in -(* -debug_print (lazy "\n\n---- BEGIN ") ; -debug_print (lazy ("----params: " ^ String.concat " ; " (List.map UriManager.string_of_uri params))) ; -debug_print (lazy ("----S(" ^ UriManager.string_of_uri uri ^ "): " ^ String.concat " ; " (List.map (function (uri,_) -> UriManager.string_of_uri uri) exp_named_subst))) ; -debug_print (lazy ("----P: " ^ String.concat " ; " (List.map (function (uri,_) -> UriManager.string_of_uri uri) exp_named_subst'))) ; -*) let exp_named_subst'' = substaux_in_exp_named_subst uri k exp_named_subst' params in -(* -debug_print (lazy ("----D: " ^ String.concat " ; " (List.map (function (uri,_) -> UriManager.string_of_uri uri) exp_named_subst''))) ; -debug_print (lazy "---- END\n\n ") ; -*) C.Var (uri,exp_named_subst'') ) | C.Meta (i, l) -> @@ -311,6 +307,14 @@ debug_print (lazy "---- END\n\n ") ; let exp_named_subst'' = substaux_in_exp_named_subst uri k exp_named_subst' params in +if (List.map fst exp_named_subst'' <> List.map fst (List.filter (fun (uri,_) -> List.mem uri params) exp_named_subst) @ List.map fst exp_named_subst') then ( +debug_print (lazy "\n\n---- BEGIN ") ; +debug_print (lazy ("----params: " ^ String.concat " ; " (List.map UriManager.string_of_uri params))) ; +debug_print (lazy ("----S(" ^ UriManager.string_of_uri uri ^ "): " ^ String.concat " ; " (List.map (function (uri,_) -> UriManager.string_of_uri uri) exp_named_subst))) ; +debug_print (lazy ("----P: " ^ String.concat " ; " (List.map (function (uri,_) -> UriManager.string_of_uri uri) exp_named_subst'))) ; +debug_print (lazy ("----D: " ^ String.concat " ; " (List.map (function (uri,_) -> UriManager.string_of_uri uri) exp_named_subst''))) ; +debug_print (lazy "---- END\n\n ") ; +); C.MutConstruct (uri,typeno,consno,exp_named_subst'') | C.MutCase (sp,i,outt,t,pl) -> C.MutCase (sp,i,substaux k outt, substaux k t, @@ -332,8 +336,6 @@ debug_print (lazy "---- END\n\n ") ; in C.CoFix (i, substitutedfl) and substaux_in_exp_named_subst uri k exp_named_subst' params = -(*CSC: invece di concatenare sarebbe meglio rispettare l'ordine dei params *) -(*CSC: e' vero???? una veloce prova non sembra confermare la teoria *) let rec filter_and_lift = function [] -> [] @@ -345,18 +347,24 @@ debug_print (lazy "---- END\n\n ") ; -> (uri,lift (k-1) t)::(filter_and_lift tl) | _::tl -> filter_and_lift tl -(* - | (uri,_)::tl -> -debug_print (lazy ("---- SKIPPO " ^ UriManager.string_of_uri uri)) ; -if List.for_all (function (uri',_) -> not (UriManager.eq uri uri')) -exp_named_subst' then debug_print (lazy "---- OK1") ; -debug_print (lazy ("++++ uri " ^ UriManager.string_of_uri uri ^ " not in " ^ String.concat " ; " (List.map UriManager.string_of_uri params))) ; -if List.mem uri params then debug_print (lazy "---- OK2") ; - filter_and_lift tl -*) in - List.map (function (uri,t) -> (uri,substaux k t)) exp_named_subst' @ - (filter_and_lift exp_named_subst) + let res = + List.map (function (uri,t) -> (uri,substaux k t)) exp_named_subst' @ + (filter_and_lift exp_named_subst) + in + let rec reorder = + function + [] -> [] + | uri::tl -> + let he = + try + [uri,List.assoc uri res] + with + Not_found -> [] + in + he@reorder tl + in + reorder params in if exp_named_subst = [] then t else substaux 1 t diff --git a/helm/software/components/cic_proof_checking/cicTypeChecker.ml b/helm/software/components/cic_proof_checking/cicTypeChecker.ml index 35015e541..88219ee37 100644 --- a/helm/software/components/cic_proof_checking/cicTypeChecker.ml +++ b/helm/software/components/cic_proof_checking/cicTypeChecker.ml @@ -1328,7 +1328,7 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = | C.Var (uri,exp_named_subst) -> incr fdebug ; let ugraph1 = - check_exp_named_subst ~logger ~subst context exp_named_subst ugraph + check_exp_named_subst uri ~logger ~subst context exp_named_subst ugraph in let ty,ugraph2 = type_of_variable ~logger uri ugraph1 in let ty1 = CicSubstitution.subst_vars exp_named_subst ty in @@ -1441,7 +1441,7 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = | C.Const (uri,exp_named_subst) -> incr fdebug ; let ugraph1 = - check_exp_named_subst ~logger ~subst context exp_named_subst ugraph + check_exp_named_subst uri ~logger ~subst context exp_named_subst ugraph in let cty,ugraph2 = type_of_constant ~logger uri ugraph1 in let cty1 = @@ -1452,11 +1452,9 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = | C.MutInd (uri,i,exp_named_subst) -> incr fdebug ; let ugraph1 = - check_exp_named_subst ~logger ~subst context exp_named_subst ugraph + check_exp_named_subst uri ~logger ~subst context exp_named_subst ugraph in - (* TASSI: da me c'era anche questa, ma in CVS no *) let mty,ugraph2 = type_of_mutual_inductive_defs ~logger uri i ugraph1 in - (* fine parte dubbia *) let cty = CicSubstitution.subst_vars exp_named_subst mty in @@ -1464,9 +1462,8 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = cty,ugraph2 | C.MutConstruct (uri,i,j,exp_named_subst) -> let ugraph1 = - check_exp_named_subst ~logger ~subst context exp_named_subst ugraph + check_exp_named_subst uri ~logger ~subst context exp_named_subst ugraph in - (* TASSI: idem come sopra *) let mty,ugraph2 = type_of_mutual_inductive_constr ~logger uri i j ugraph1 in @@ -1773,7 +1770,24 @@ end; let (_,ty,_) = List.nth fl i in ty,ugraph2 - and check_exp_named_subst ~logger ~subst context = + and check_exp_named_subst uri ~logger ~subst context ens ugraph = + let params = + let obj,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in + (match obj with + Cic.Constant (_,_,_,params,_) -> params + | Cic.Variable (_,_,_,params,_) -> params + | Cic.CurrentProof (_,_,_,_,params,_) -> params + | Cic.InductiveDefinition (_,params,_,_) -> params + ) in + let rec check_same_order params ens = + match params,ens with + | _,[] -> () + | [],_::_ -> + raise (TypeCheckerFailure (lazy "Bad explicit named substitution")) + | uri::tl,(uri',_)::tl' when UriManager.eq uri uri' -> + check_same_order tl tl' + | _::tl,l -> check_same_order tl l + in let rec check_exp_named_subst_aux ~logger esubsts l ugraph = match l with [] -> ugraph @@ -1799,7 +1813,8 @@ end; raise (TypeCheckerFailure (lazy "Wrong Explicit Named Substitution")) end in - check_exp_named_subst_aux ~logger [] + check_same_order params ens ; + check_exp_named_subst_aux ~logger [] ens ugraph and sort_of_prod ~subst context (name,s) (t1, t2) ugraph = let module C = Cic in diff --git a/helm/software/components/ng_kernel/TEST b/helm/software/components/ng_kernel/TEST index 933460b8d..6f3d571a1 100644 --- a/helm/software/components/ng_kernel/TEST +++ b/helm/software/components/ng_kernel/TEST @@ -29,18 +29,18 @@ Rocq/COC: type-checking vecchio nucleo troppo lento nijmegen: type-checking vecchio nucleo troppo lento Sophia-Antipolis/Float: vecchio nucleo troppo lento Sophia-Antipolis/geometry: vecchio nucleo troppo lento +Rocq/ALGEBRA/CATEGORY_THEORY: vecchio nucleo troppo lento matita/tests: nuovo nucleo problema con universi!!! +cic:/Rocq/ALGEBRA/CATEGORY_THEORY/LIMITS/FunForget_UA/UA_FM.con: 15.17s vs 0.14s vecchio nucleo! coq: nuovo nucleo mooooolto lento in guarded by: cic:/Coq/ZArith/Zsqrt/sqrtrempos.con orsay: nuovo nucleo diverge (vedi sopra) Sophia-Antipolis/Buchberger: nuovo nucleo diverge matita/freescale: nuovo nucleo diverge -Rocq/ALGEBRA/CATEGORY_THEORY: vecchio nucleo: ??? - cic:/Rocq/ALGEBRA/CATEGORY_THEORY/ADJUNCTION/Adj_FunFreeMon/Adj_FunFreeMon_FunForget.con -Sophia-Antipolis/Algebra: vecchio nucleo variabili -lyon/PROCESSES: vecchio nucleo, variabili +Sophia-Antipolis/Algebra: nuovo nucleo? +lyon/PROCESSES: nuovo nucleo? lannion: nuovo nucleo impredicative set rocq.higman: nuovo nucleo impredicative set -- 2.39.2