From 9b57abaabd8f66607062c3f33e74928f61468060 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 22 Mar 2007 19:04:32 +0000 Subject: [PATCH] Several instances of the same bug fixed at once: when processing a Fix, before adding the types to the context (to process the bodies), the types must be lifted. The simplify tactic is still not working propertly. --- helm/software/components/cic_acic/cic2acic.ml | 34 ++++++--- .../cic_proof_checking/cicReduction.ml | 18 +++-- .../cic_proof_checking/cicTypeChecker.ml | 69 +++++++++++++++---- .../cic_proof_checking/freshNamesGenerator.ml | 20 ++++-- .../tactics/proofEngineReduction.ml | 32 ++++++--- 5 files changed, 132 insertions(+), 41 deletions(-) diff --git a/helm/software/components/cic_acic/cic2acic.ml b/helm/software/components/cic_acic/cic2acic.ml index d8392f620..98b142982 100644 --- a/helm/software/components/cic_acic/cic2acic.ml +++ b/helm/software/components/cic_acic/cic2acic.ml @@ -353,8 +353,12 @@ let acic_of_cic_context' ~computeinnertypes:global_computeinnertypes let fresh_idrefs = List.map (function _ -> gen_id seed) funs in let new_idrefs = List.rev fresh_idrefs @ idrefs in - let tys = - List.map (fun (name,_,ty,_) -> Some (C.Name name, C.Decl ty)) funs + let tys,_ = + List.fold_left + (fun (types,len) (n,_,ty,_) -> + (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, + len+1) + ) ([],0) funs in xxx_add ids_to_inner_sorts fresh_id'' innersort ; if innersort = `Prop then @@ -370,8 +374,12 @@ let acic_of_cic_context' ~computeinnertypes:global_computeinnertypes let fresh_idrefs = List.map (function _ -> gen_id seed) funs in let new_idrefs = List.rev fresh_idrefs @ idrefs in - let tys = - List.map (fun (name,ty,_) -> Some (C.Name name, C.Decl ty)) funs + let tys,_ = + List.fold_left + (fun (types,len) (n,ty,_) -> + (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, + len+1) + ) ([],0) funs in xxx_add ids_to_inner_sorts fresh_id'' innersort ; if innersort = `Prop then @@ -687,9 +695,12 @@ let plain_acic_term_of_cic_term = C.AMutCase (fresh_id, uri, tyno, aux context outty, aux context term, List.map (aux context) patterns) | C.Fix (funno, funs) -> - let tys = - List.map - (fun (name,_,ty,_) -> mk_fresh_id (), Some (C.Name name, C.Decl ty)) funs + let tys,_ = + List.fold_left + (fun (types,len) (n,_,ty,_) -> + (mk_fresh_id (),(Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))))::types, + len+1 + ) ([],0) funs in C.AFix (fresh_id, funno, List.map2 @@ -698,9 +709,12 @@ let plain_acic_term_of_cic_term = ) tys funs ) | C.CoFix (funno, funs) -> - let tys = - List.map (fun (name,ty,_) -> - mk_fresh_id (),Some (C.Name name, C.Decl ty)) funs + let tys,_ = + List.fold_left + (fun (types,len) (n,ty,_) -> + (mk_fresh_id (),(Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))))::types, + len+1 + ) ([],0) funs in C.ACoFix (fresh_id, funno, List.map2 diff --git a/helm/software/components/cic_proof_checking/cicReduction.ml b/helm/software/components/cic_proof_checking/cicReduction.ml index 576721be3..bfba135cf 100644 --- a/helm/software/components/cic_proof_checking/cicReduction.ml +++ b/helm/software/components/cic_proof_checking/cicReduction.ml @@ -973,8 +973,12 @@ prerr_endline ("%%%%%%: " ^ CicPp.ppterm term' ^ " <==> " ^ CicPp.ppterm t1); else false,ugraph | (C.Fix (i1,fl1), C.Fix (i2,fl2)) -> - let tys = - List.map (function (n,_,ty,_) -> Some (C.Name n,(C.Decl ty))) fl1 + let tys,_ = + List.fold_left + (fun (types,len) (n,_,ty,_) -> + (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, + len+1) + ) ([],0) fl1 in if i1 = i2 then List.fold_right2 @@ -992,9 +996,13 @@ prerr_endline ("%%%%%%: " ^ CicPp.ppterm term' ^ " <==> " ^ CicPp.ppterm t1); else false,ugraph | (C.CoFix (i1,fl1), C.CoFix (i2,fl2)) -> - let tys = - List.map (function (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl1 - in + let tys,_ = + List.fold_left + (fun (types,len) (n,ty,_) -> + (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, + len+1) + ) ([],0) fl1 + in if i1 = i2 then List.fold_right2 (fun (_,ty1,bo1) (_,ty2,bo2) (b,ugraph) -> diff --git a/helm/software/components/cic_proof_checking/cicTypeChecker.ml b/helm/software/components/cic_proof_checking/cicTypeChecker.ml index 5dc425489..b57ad4e78 100644 --- a/helm/software/components/cic_proof_checking/cicTypeChecker.ml +++ b/helm/software/components/cic_proof_checking/cicTypeChecker.ml @@ -292,8 +292,12 @@ and does_not_occur ?(subst=[]) context n nn te = let len = List.length fl in let n_plus_len = n + len in let nn_plus_len = nn + len in - let tys = - List.map (fun (n,_,ty,_) -> Some (C.Name n,(Cic.Decl ty))) fl + let tys,_ = + List.fold_left + (fun (types,len) (n,_,ty,_) -> + (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, + len+1) + ) ([],0) fl in List.fold_right (fun (_,_,ty,bo) i -> @@ -304,8 +308,12 @@ and does_not_occur ?(subst=[]) context n nn te = let len = List.length fl in let n_plus_len = n + len in let nn_plus_len = nn + len in - let tys = - List.map (fun (n,ty,_) -> Some (C.Name n,(Cic.Decl ty))) fl + let tys,_ = + List.fold_left + (fun (types,len) (n,ty,_) -> + (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, + len+1) + ) ([],0) fl in List.fold_right (fun (_,ty,bo) i -> @@ -886,7 +894,12 @@ and check_is_really_smaller_arg ~subst context n nn kl x safes te = let n_plus_len = n + len and nn_plus_len = nn + len and x_plus_len = x + len - and tys = List.map (fun (n,_,ty,_) -> Some (C.Name n,(C.Decl ty))) fl + and tys,_ = + List.fold_left + (fun (types,len) (n,_,ty,_) -> + (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, + len+1) + ) ([],0) fl and safes' = List.map (fun x -> x + len) safes in List.fold_right (fun (_,_,ty,bo) i -> @@ -899,7 +912,12 @@ and check_is_really_smaller_arg ~subst context n nn kl x safes te = let n_plus_len = n + len and nn_plus_len = nn + len and x_plus_len = x + len - and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl + and tys,_ = + List.fold_left + (fun (types,len) (n,ty,_) -> + (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, + len+1) + ) ([],0) fl and safes' = List.map (fun x -> x + len) safes in List.fold_right (fun (_,ty,bo) i -> @@ -1091,7 +1109,12 @@ and guarded_by_destructors ~subst context n nn kl x safes = let n_plus_len = n + len and nn_plus_len = nn + len and x_plus_len = x + len - and tys = List.map (fun (n,_,ty,_) -> Some (C.Name n,(C.Decl ty))) fl + and tys,_ = + List.fold_left + (fun (types,len) (n,_,ty,_) -> + (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, + len+1) + ) ([],0) fl and safes' = List.map (fun x -> x + len) safes in List.fold_right (fun (_,_,ty,bo) i -> @@ -1104,7 +1127,12 @@ and guarded_by_destructors ~subst context n nn kl x safes = let n_plus_len = n + len and nn_plus_len = nn + len and x_plus_len = x + len - and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl + and tys,_ = + List.fold_left + (fun (types,len) (n,ty,_) -> + (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, + len+1) + ) ([],0) fl and safes' = List.map (fun x -> x + len) safes in List.fold_right (fun (_,ty,bo) i -> @@ -1257,7 +1285,13 @@ and guarded_by_constructors ~subst 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.fold_left + (fun (types,len) (n,ty,_) -> + (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, + len+1) + ) ([],0) fl + in List.fold_right (fun (_,ty,bo) i -> i && does_not_occur ~subst context n nn ty && @@ -1298,7 +1332,13 @@ and guarded_by_constructors ~subst 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.fold_left + (fun (types,len) (n,_,ty,_) -> + (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, + len+1) + ) ([],0) fl + in List.fold_right (fun (_,_,ty,bo) i -> i && does_not_occur ~subst context n nn ty && @@ -1309,7 +1349,13 @@ and guarded_by_constructors ~subst 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.fold_left + (fun (types,len) (n,ty,_) -> + (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, + len+1) + ) ([],0) fl + in List.fold_right (fun (_,ty,bo) i -> i && does_not_occur ~subst context n nn ty && @@ -1835,7 +1881,6 @@ end; outtype,ugraph5 | C.Fix (i,fl) -> let types,kl,ugraph1,len = - (* WAS: list rev list map *) List.fold_left (fun (types,kl,ugraph,len) (n,k,ty,_) -> let _,ugraph1 = type_of_aux ~logger context ty ugraph in diff --git a/helm/software/components/cic_proof_checking/freshNamesGenerator.ml b/helm/software/components/cic_proof_checking/freshNamesGenerator.ml index 3cfda02df..73b75ce18 100755 --- a/helm/software/components/cic_proof_checking/freshNamesGenerator.ml +++ b/helm/software/components/cic_proof_checking/freshNamesGenerator.ml @@ -193,9 +193,13 @@ let rec mk_fresh_names ~subst metasenv context t = let pl' = List.map (mk_fresh_names ~subst metasenv context) pl in Cic.MutCase (sp, i, outty', t', pl') | Cic.Fix (i, fl) -> - let tys = List.map - (fun (n,_,ty,_) -> - Some (Cic.Name n,(Cic.Decl ty))) fl in + let tys,_ = + List.fold_left + (fun (types,len) (n,_,ty,_) -> + (Some (Cic.Name n,(Cic.Decl (CicSubstitution.lift len ty)))::types, + len+1) + ) ([],0) fl + in let fl' = List.map (fun (n,i,ty,bo) -> let ty' = mk_fresh_names ~subst metasenv context ty in @@ -203,9 +207,13 @@ let rec mk_fresh_names ~subst metasenv context t = (n,i,ty',bo')) fl in Cic.Fix (i, fl') | Cic.CoFix (i, fl) -> - let tys = List.map - (fun (n,_,ty) -> - Some (Cic.Name n,(Cic.Decl ty))) fl in + let tys,_ = + List.fold_left + (fun (types,len) (n,ty,_) -> + (Some (Cic.Name n,(Cic.Decl (CicSubstitution.lift len ty)))::types, + len+1) + ) ([],0) fl + in let fl' = List.map (fun (n,ty,bo) -> let ty' = mk_fresh_names ~subst metasenv context ty in diff --git a/helm/software/components/tactics/proofEngineReduction.ml b/helm/software/components/tactics/proofEngineReduction.ml index 1b5922d1d..f72ec4679 100644 --- a/helm/software/components/tactics/proofEngineReduction.ml +++ b/helm/software/components/tactics/proofEngineReduction.ml @@ -587,8 +587,12 @@ let reduce context = if l = [] then res else C.Appl (res::l) ) | C.Fix (i,fl) -> - let tys = - List.map (function (name,_,ty,_) -> Some (C.Name name, C.Decl ty)) fl + let tys,_ = + List.fold_left + (fun (types,len) (n,_,ty,_) -> + (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, + len+1) + ) ([],0) fl in let t' () = let fl' = @@ -625,8 +629,12 @@ let reduce context = | None -> if l = [] then t' () else C.Appl ((t' ())::l) ) | C.CoFix (i,fl) -> - let tys = - List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl + let tys,_ = + List.fold_left + (fun (types,len) (n,ty,_) -> + (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, + len+1) + ) ([],0) fl in let t' = let fl' = @@ -819,8 +827,12 @@ let simpl context = if l = [] then res else C.Appl (res::l) ) | C.Fix (i,fl) -> - let tys = - List.map (function (name,_,ty,_) -> Some (C.Name name, C.Decl ty)) fl + let tys,_ = + List.fold_left + (fun (types,len) (n,_,ty,_) -> + (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, + len+1) + ) ([],0) fl in let t' () = let fl' = @@ -857,8 +869,12 @@ let simpl context = | None -> if l = [] then t' () else C.Appl ((t' ())::l) ) | C.CoFix (i,fl) -> - let tys = - List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl + let tys,_ = + List.fold_left + (fun (types,len) (n,ty,_) -> + (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, + len+1) + ) ([],0) fl in let t' = let fl' = -- 2.39.2