From 4adceafdaa4cd82c427ac9de494179c242e7ad28 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Thu, 15 Apr 2004 16:47:42 +0000 Subject: [PATCH] Metasenv added as parameter to eta_fixing. --- helm/ocaml/cic_omdoc/cic2acic.ml | 51 ++++++++++++----------- helm/ocaml/cic_omdoc/eta_fixing.ml | 63 +++++++++++++---------------- helm/ocaml/cic_omdoc/eta_fixing.mli | 2 +- 3 files changed, 53 insertions(+), 63 deletions(-) diff --git a/helm/ocaml/cic_omdoc/cic2acic.ml b/helm/ocaml/cic_omdoc/cic2acic.ml index 495cb0405..bf686ac4e 100644 --- a/helm/ocaml/cic_omdoc/cic2acic.ml +++ b/helm/ocaml/cic_omdoc/cic2acic.ml @@ -414,30 +414,30 @@ let acic_object_of_cic_object ?(eta_fix=true) obj = let aconjecture_of_conjecture' = aconjecture_of_conjecture seed ids_to_terms ids_to_father_ids ids_to_inner_sorts ids_to_inner_types ids_to_hypotheses hypotheses_seed in - let eta_fix metasenv t = - if eta_fix then E.eta_fix metasenv t else t + let eta_fix metasenv context t = + if eta_fix then E.eta_fix metasenv context t else t in let aobj = match obj with C.Constant (id,Some bo,ty,params) -> - let bo' = eta_fix [] bo in - let ty' = eta_fix [] ty in + let bo' = eta_fix [] [] bo in + let ty' = eta_fix [] [] ty in let abo = acic_term_of_cic_term' bo' (Some ty') in let aty = acic_term_of_cic_term' ty' None in C.AConstant ("mettereaposto",Some "mettereaposto2",id,Some abo,aty,params) | C.Constant (id,None,ty,params) -> - let ty' = eta_fix [] ty in + let ty' = eta_fix [] [] ty in let aty = acic_term_of_cic_term' ty' None in C.AConstant ("mettereaposto",None,id,None,aty,params) | C.Variable (id,bo,ty,params) -> - let ty' = eta_fix [] ty in + let ty' = eta_fix [] [] ty in let abo = match bo with None -> None | Some bo -> - let bo' = eta_fix [] bo in + let bo' = eta_fix [] [] bo in Some (acic_term_of_cic_term' bo' (Some ty')) in let aty = acic_term_of_cic_term' ty' None in @@ -445,28 +445,27 @@ let acic_object_of_cic_object ?(eta_fix=true) obj = ("mettereaposto",id,abo,aty, params) | C.CurrentProof (id,conjectures,bo,ty,params) -> let conjectures' = - (*CSC: This code is bugged, since it does a List.map instead - * of a List.fold, withouth calling eta_fixing with the - * current context. Indeed, eta_fix always starts now in the - * empty context. Instead of fixing this piece of code and - * adding a new argument to eta_fix, I just skip eta_fixing - * of the CurrentProof metasenv. Does this break well-typedness? List.map (function (i,canonical_context,term) -> let canonical_context' = - List.map - (function - None -> None - | Some (n, C.Decl t)-> Some (n, C.Decl (eta_fix conjectures t)) - | Some (n, C.Def (t,None)) -> - Some (n, C.Def ((eta_fix conjectures t),None)) - | Some (_,C.Def (_,Some _)) -> assert false - ) canonical_context + List.fold_right + (fun d canonical_context' -> + let d' = + match d with + None -> None + | Some (n, C.Decl t)-> + Some (n, C.Decl (eta_fix conjectures canonical_context' t)) + | Some (n, C.Def (t,None)) -> + Some (n, + C.Def ((eta_fix conjectures canonical_context' t),None)) + | Some (_,C.Def (_,Some _)) -> assert false + in + d::canonical_context' + ) [] canonical_context in - let term' = eta_fix conjectures term in + let term' = eta_fix conjectures canonical_context' term in (i,canonical_context',term') - ) conjectures *) - conjectures + ) conjectures in let aconjectures = List.map @@ -519,8 +518,8 @@ let acic_object_of_cic_object ?(eta_fix=true) obj = (cid,i,(List.rev revacanonical_context),aterm) ) conjectures' in *) let time1 = Sys.time () in - let bo' = eta_fix conjectures' bo in - let ty' = eta_fix conjectures' ty in + let bo' = eta_fix conjectures' [] bo in + let ty' = eta_fix conjectures' [] ty in let time2 = Sys.time () in prerr_endline ("++++++++++ Tempi della eta_fix: "^ string_of_float (time2 -. time1)) ; diff --git a/helm/ocaml/cic_omdoc/eta_fixing.ml b/helm/ocaml/cic_omdoc/eta_fixing.ml index 9b2072910..6d5ce9833 100644 --- a/helm/ocaml/cic_omdoc/eta_fixing.ml +++ b/helm/ocaml/cic_omdoc/eta_fixing.ml @@ -23,9 +23,7 @@ * http://cs.unibo.it/helm/. *) -exception ReferenceToVariable;; -exception RferenceToCurrentProof;; -exception ReferenceToInductiveDefinition;; +exception ReferenceToNonVariable;; let prerr_endline _ = ();; @@ -132,7 +130,11 @@ let fix_according_to_type ty hd tl = let rec aux n ty tl res = if n = 0 then (match tl with - [] -> C.Appl res + [] -> + (match res with + [] -> assert false + | [res] -> res + | _ -> C.Appl res) | _ -> match res with [] -> assert false @@ -163,7 +165,7 @@ let fix_according_to_type ty hd tl = aux expected_arity ty tl [hd] ;; -let eta_fix metasenv t = +let eta_fix metasenv context t = let rec eta_fix' context t = (* prerr_endline ("entering aux with: term=" ^ CicPp.ppterm t); flush stderr ; *) @@ -172,11 +174,8 @@ let eta_fix metasenv t = match t with C.Rel n -> C.Rel n | C.Var (uri,exp_named_subst) -> - let exp_named_subst' = - List.map - (function i,t -> i, (eta_fix' context t)) exp_named_subst - in - C.Var (uri,exp_named_subst') + let exp_named_subst' = fix_exp_named_subst context exp_named_subst in + C.Var (uri,exp_named_subst') | C.Meta (n,l) -> let (_,canonical_context,_) = List.find (function (m,_,_) -> n = m) metasenv @@ -224,22 +223,13 @@ let eta_fix metasenv t = constant_type (C.Const(uri,exp_named_subst)) l'' | _ -> C.Appl l' *)) | C.Const (uri,exp_named_subst) -> - let exp_named_subst' = - List.map - (function i,t -> i, (eta_fix' context t)) exp_named_subst - in - C.Const (uri,exp_named_subst') + let exp_named_subst' = fix_exp_named_subst context exp_named_subst in + C.Const (uri,exp_named_subst') | C.MutInd (uri,tyno,exp_named_subst) -> - let exp_named_subst' = - List.map - (function i,t -> i, (eta_fix' context t)) exp_named_subst - in + let exp_named_subst' = fix_exp_named_subst context exp_named_subst in C.MutInd (uri, tyno, exp_named_subst') | C.MutConstruct (uri,tyno,consno,exp_named_subst) -> - let exp_named_subst' = - List.map - (function i,t -> i, (eta_fix' context t)) exp_named_subst - in + let exp_named_subst' = fix_exp_named_subst context exp_named_subst in C.MutConstruct (uri, tyno, consno, exp_named_subst') | C.MutCase (uri, tyno, outty, term, patterns) as prima -> let outty' = eta_fix' context outty in @@ -298,17 +288,18 @@ let eta_fix metasenv t = List.map (fun (name, ty, bo) -> (name, eta_fix' context ty, eta_fix' (fun_types@context) bo)) funs) - in - eta_fix' [] t + and fix_exp_named_subst context exp_named_subst = + List.rev + (List.fold_left + (fun newsubst (uri,t) -> + let t' = eta_fix' context t in + let ty = + match CicEnvironment.get_obj uri with + Cic.Variable (_,_,ty,_) -> CicSubstitution.subst_vars newsubst ty + | _ -> raise ReferenceToNonVariable in + let t'' = fix_according_to_type ty t' [] in + (uri,t'')::newsubst + ) [] exp_named_subst) + in + eta_fix' context t ;; - - - - - - - - - - - diff --git a/helm/ocaml/cic_omdoc/eta_fixing.mli b/helm/ocaml/cic_omdoc/eta_fixing.mli index 6da260aab..c6c68119d 100644 --- a/helm/ocaml/cic_omdoc/eta_fixing.mli +++ b/helm/ocaml/cic_omdoc/eta_fixing.mli @@ -23,6 +23,6 @@ * http://cs.unibo.it/helm/. *) -val eta_fix : Cic.metasenv -> Cic.term -> Cic.term +val eta_fix : Cic.metasenv -> Cic.context -> Cic.term -> Cic.term -- 2.39.2