From 05602d605a8a694dc5c3f4a517810c027e20dc2f Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Sun, 22 Dec 2002 19:04:49 +0000 Subject: [PATCH] * First implementation of CicRefine * unwind_subst is now exported in the interface --- helm/ocaml/cic_unification/.depend | 3 + helm/ocaml/cic_unification/Makefile | 2 +- helm/ocaml/cic_unification/cicRefine.ml | 354 ++++++++++++++++++ helm/ocaml/cic_unification/cicRefine.mli | 39 ++ helm/ocaml/cic_unification/cicUnification.mli | 7 + 5 files changed, 404 insertions(+), 1 deletion(-) create mode 100644 helm/ocaml/cic_unification/cicRefine.ml create mode 100644 helm/ocaml/cic_unification/cicRefine.mli diff --git a/helm/ocaml/cic_unification/.depend b/helm/ocaml/cic_unification/.depend index 31eaf6dd0..d22689dce 100644 --- a/helm/ocaml/cic_unification/.depend +++ b/helm/ocaml/cic_unification/.depend @@ -1,2 +1,5 @@ +cicRefine.cmi: cicUnification.cmi cicUnification.cmo: cicUnification.cmi cicUnification.cmx: cicUnification.cmi +cicRefine.cmo: cicUnification.cmi cicRefine.cmi +cicRefine.cmx: cicUnification.cmx cicRefine.cmi diff --git a/helm/ocaml/cic_unification/Makefile b/helm/ocaml/cic_unification/Makefile index 5a88cbb4d..fbf0d22ed 100644 --- a/helm/ocaml/cic_unification/Makefile +++ b/helm/ocaml/cic_unification/Makefile @@ -2,7 +2,7 @@ PACKAGE = cic_unification REQUIRES = helm-cic_proof_checking PREDICATES = -INTERFACE_FILES = cicUnification.mli +INTERFACE_FILES = cicUnification.mli cicRefine.mli IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) EXTRA_OBJECTS_TO_INSTALL = diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml new file mode 100644 index 000000000..f7a0ab2e8 --- /dev/null +++ b/helm/ocaml/cic_unification/cicRefine.ml @@ -0,0 +1,354 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +exception Impossible of int;; +exception NotRefinable of string;; +exception WrongUriToConstant of string;; +exception WrongUriToVariable of string;; +exception WrongUriToMutualInductiveDefinitions of string;; +exception RelToHiddenHypothesis;; +exception MetasenvInconsistency;; +exception MutCaseFixAndCofixRefineNotImplemented;; +exception FreeMetaFound of int;; + +let fdebug = ref 0;; +let debug t context = + let rec debug_aux t i = + let module C = Cic in + let module U = UriManager in + CicPp.ppobj (C.Variable ("DEBUG", None, t, [])) ^ "\n" ^ i + in + if !fdebug = 0 then + raise (NotRefinable ("\n" ^ List.fold_right debug_aux (t::context) "")) + (*print_endline ("\n" ^ List.fold_right debug_aux (t::context) "") ; flush stdout*) +;; + +let rec type_of_constant uri = + let module C = Cic in + let module R = CicReduction in + let module U = UriManager in + match CicEnvironment.get_cooked_obj uri with + C.Constant (_,_,ty,_) -> ty + | C.CurrentProof (_,_,_,ty,_) -> ty + | _ -> raise (WrongUriToConstant (U.string_of_uri uri)) + +and type_of_variable uri = + let module C = Cic in + let module R = CicReduction in + let module U = UriManager in + match CicEnvironment.get_cooked_obj uri with + C.Variable (_,_,ty,_) -> ty + | _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri)) + +and type_of_mutual_inductive_defs uri i = + let module C = Cic in + let module R = CicReduction in + let module U = UriManager in + match CicEnvironment.get_cooked_obj uri with + C.InductiveDefinition (dl,_,_) -> + let (_,_,arity,_) = List.nth dl i in + arity + | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri)) + +and type_of_mutual_inductive_constr uri i j = + let module C = Cic in + let module R = CicReduction in + let module U = UriManager in + match CicEnvironment.get_cooked_obj uri with + C.InductiveDefinition (dl,_,_) -> + let (_,_,_,cl) = List.nth dl i in + let (_,ty) = List.nth cl (j-1) in + ty + | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri)) + +(* type_of_aux' is just another name (with a different scope) for type_of_aux *) +and type_of_aux' metasenv context t = + let rec type_of_aux subst metasenv context = + let module C = Cic in + let module S = CicSubstitution in + let module U = UriManager in + let module Un = CicUnification in + function + C.Rel n -> + (try + match List.nth context (n - 1) with + Some (_,C.Decl t) -> S.lift n t,subst,metasenv + | Some (_,C.Def bo) -> + type_of_aux subst metasenv context (S.lift n bo) + | None -> raise RelToHiddenHypothesis + with + _ -> raise (NotRefinable "Not a close term") + ) + | C.Var (uri,exp_named_subst) -> + incr fdebug ; + let subst',metasenv' = + check_exp_named_subst subst metasenv context exp_named_subst in + let ty = + CicSubstitution.subst_vars exp_named_subst (type_of_variable uri) + in + decr fdebug ; + ty,subst',metasenv' + | C.Meta (n,l) -> + let (_,canonical_context,ty) = + try + List.find (function (m,_,_) -> n = m) metasenv + with + Not_found -> raise (FreeMetaFound n) + in + let subst',metasenv' = + check_metasenv_consistency subst metasenv context canonical_context l + in + CicSubstitution.lift_meta l ty, subst', metasenv' + | C.Sort s -> + C.Sort C.Type, (*CSC manca la gestione degli universi!!! *) + subst,metasenv + | C.Implicit -> raise (Impossible 21) + | C.Cast (te,ty) -> + let _,subst',metasenv' = + type_of_aux subst metasenv context ty in + let inferredty,subst'',metasenv'' = + type_of_aux subst' metasenv' context ty + in + (try + let subst''',metasenv''' = + Un.fo_unif_subst subst'' context metasenv'' inferredty ty + in + ty,subst''',metasenv''' + with + _ -> raise (NotRefinable "Cast")) + | C.Prod (name,s,t) -> + let sort1,subst',metasenv' = type_of_aux subst metasenv context s in + let sort2,subst'',metasenv'' = + type_of_aux subst' metasenv' ((Some (name,(C.Decl s)))::context) t + in + sort_of_prod subst'' metasenv'' context (name,s) (sort1,sort2) + | C.Lambda (n,s,t) -> + let sort1,subst',metasenv' = type_of_aux subst metasenv context s in + let type2,subst'',metasenv'' = + type_of_aux subst' metasenv' ((Some (n,(C.Decl s)))::context) t + in + let sort2,subst''',metasenv''' = + type_of_aux subst'' metasenv''((Some (n,(C.Decl s)))::context) type2 + in + (* only to check if the product is well-typed *) + let _,subst'''',metasenv'''' = + sort_of_prod subst''' metasenv''' context (n,s) (sort1,sort2) + in + 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 inferredty,subst'',metasenv'' = + type_of_aux subst' metasenv' ((Some (n,(C.Def s)))::context) t + in + (* One-step LetIn reduction. Even faster than the previous solution. + Moreover the inferred type is closer to the expected one. *) + CicSubstitution.subst s inferredty,subst',metasenv' + | C.Appl (he::tl) when List.length tl > 0 -> + let hetype,subst',metasenv' = type_of_aux subst metasenv context he in + let tlbody_and_type,subst'',metasenv'' = + List.fold_right + (fun x (res,subst,metasenv) -> + let ty,subst',metasenv' = + type_of_aux subst metasenv context x + in + (x, ty)::res,subst',metasenv' + ) tl ([],subst',metasenv') + in + eat_prods subst'' metasenv'' context hetype tlbody_and_type + | C.Appl _ -> raise (NotRefinable "Appl: no arguments") + | C.Const (uri,exp_named_subst) -> + incr fdebug ; + let subst',metasenv' = + check_exp_named_subst subst metasenv context exp_named_subst in + let cty = + CicSubstitution.subst_vars exp_named_subst (type_of_constant uri) + in + decr fdebug ; + cty,subst',metasenv' + | C.MutInd (uri,i,exp_named_subst) -> + incr fdebug ; + let subst',metasenv' = + check_exp_named_subst subst metasenv context exp_named_subst in + let cty = + CicSubstitution.subst_vars exp_named_subst + (type_of_mutual_inductive_defs uri i) + in + decr fdebug ; + cty,subst',metasenv' + | C.MutConstruct (uri,i,j,exp_named_subst) -> + let subst',metasenv' = + check_exp_named_subst subst metasenv context exp_named_subst in + let cty = + CicSubstitution.subst_vars exp_named_subst + (type_of_mutual_inductive_constr uri i j) + in + cty,subst',metasenv' + | C.MutCase _ + | C.Fix _ + | C.CoFix _ -> raise MutCaseFixAndCofixRefineNotImplemented + + (* check_metasenv_consistency checks that the "canonical" context of a + metavariable is consitent - up to relocation via the relocation list l - + with the actual context *) + and check_metasenv_consistency subst metasenv context canonical_context l = + let module C = Cic in + let module R = CicReduction in + let module S = CicSubstitution in + let lifted_canonical_context = + let rec aux i = + function + [] -> [] + | (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) + | None::tl -> None::(aux (i+1) tl) + in + aux 1 canonical_context + in + List.fold_left2 + (fun (subst,metasenv) t ct -> + match (t,ct) with + _,None -> subst,metasenv + | Some t,Some (_,C.Def ct) -> + (try + CicUnification.fo_unif_subst subst context metasenv t ct + with _ -> raise MetasenvInconsistency) + | Some t,Some (_,C.Decl ct) -> + let inferredty,subst',metasenv' = + type_of_aux subst metasenv context t + in + (try + CicUnification.fo_unif_subst subst context metasenv inferredty ct + with _ -> raise MetasenvInconsistency) + | _, _ -> raise MetasenvInconsistency + ) (subst,metasenv) l lifted_canonical_context + + and check_exp_named_subst metasubst metasenv context = + let rec check_exp_named_subst_aux metasubst metasenv substs = + function + [] -> metasubst,metasenv + | ((uri,t) as subst)::tl -> + let typeofvar = + CicSubstitution.subst_vars substs (type_of_variable uri) in + (match CicEnvironment.get_cooked_obj ~trust:false uri with + Cic.Variable (_,Some bo,_,_) -> + raise + (NotRefinable + "A variable with a body can not be explicit substituted") + | Cic.Variable (_,None,_,_) -> () + | _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri)) + ) ; + let typeoft,metasubst',metasenv' = + type_of_aux metasubst metasenv context t + in + try + let metasubst'',metasenv'' = + CicUnification.fo_unif_subst + metasubst' context metasenv' typeoft typeofvar + in + check_exp_named_subst_aux metasubst'' metasenv'' (substs@[subst]) tl + with _ -> + raise (NotRefinable "Wrong Explicit Named Substitution") + in + check_exp_named_subst_aux metasubst metasenv [] + + and sort_of_prod subst metasenv context (name,s) (t1, t2) = + let module C = Cic in + (* ti could be a metavariable in the domain of the substitution *) + let subst',metasenv' = CicUnification.unwind_subst metasenv subst in + let t1' = CicUnification.apply_subst subst' t1 in + let t2' = CicUnification.apply_subst subst' t2 in + let t1'' = CicReduction.whd context t1' in + let t2'' = CicReduction.whd ((Some (name,C.Decl s))::context) t2' in + match (t1'', t2'') with + (C.Sort s1, C.Sort s2) + when (s2 = C.Prop or s2 = C.Set) -> (* different from Coq manual!!! *) + C.Sort s2,subst',metasenv' + | (C.Sort s1, C.Sort s2) -> + (*CSC manca la gestione degli universi!!! *) + C.Sort C.Type,subst',metasenv' + | (_,_) -> + raise + (NotRefinable + ("Prod: sort1= "^ CicPp.ppterm t1'' ^ " ; sort2= "^ CicPp.ppterm t2'')) + + and eat_prods subst metasenv context hetype = + function + [] -> hetype,subst,metasenv + | (hete, hety)::tl -> + (match (CicReduction.whd context hetype) with + Cic.Prod (n,s,t) -> + let subst',metasenv' = + try + CicUnification.fo_unif_subst subst context metasenv s hety + with _ -> + raise (NotRefinable "Appl: wrong parameter-type") + in + CicReduction.fdebug := -1 ; + eat_prods subst' metasenv' context (CicSubstitution.subst hete t) tl + | _ -> raise (NotRefinable "Appl: wrong Prod-type") + ) + in + let ty,subst',metasenv' = + type_of_aux [] metasenv context t + in + let subst'',metasenv'' = CicUnification.unwind_subst metasenv' subst' in + (* we get rid of the metavariables that have been instantiated *) + let metasenv''' = + List.filter + (function (i,_,_) -> not (List.exists (function (j,_) -> j=i) subst'')) + metasenv'' + in + CicUnification.apply_subst subst'' t, + CicUnification.apply_subst subst'' ty, + subst'', metasenv''' +;; + +(* DEBUGGING ONLY *) +let type_of_aux' metasenv context term = + try + let (t,ty,s,m) = + type_of_aux' metasenv context term + in + List.iter + (function (i,t) -> + prerr_endline ("+ ?" ^ string_of_int i ^ " := " ^ CicPp.ppterm t)) s ; + List.iter + (function (i,_,t) -> + prerr_endline ("+ ?" ^ string_of_int i ^ " : " ^ CicPp.ppterm t)) m ; + prerr_endline + ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty) ; + (t,ty,s,m) + with + e -> + List.iter + (function (i,_,t) -> + prerr_endline ("+ ?" ^ string_of_int i ^ " : " ^ CicPp.ppterm t)) + metasenv ; + prerr_endline ("@@@ REFINE FAILED: " ^ Printexc.to_string e) ; + raise e +;; diff --git a/helm/ocaml/cic_unification/cicRefine.mli b/helm/ocaml/cic_unification/cicRefine.mli new file mode 100644 index 000000000..18884bb12 --- /dev/null +++ b/helm/ocaml/cic_unification/cicRefine.mli @@ -0,0 +1,39 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +exception NotRefinable of string +exception WrongUriToConstant of string +exception WrongUriToVariable of string +exception WrongUriToMutualInductiveDefinitions of string +exception MutCaseFixAndCofixRefineNotImplemented;; +exception FreeMetaFound of int;; + +(* type_of_aux' metasenv context term *) +(* refines [term] and returns the refined form of [term], *) +(* its type, the computed substitution and the new metasenv. *) +(* The substitution returned is already unwinded *) +val type_of_aux': + Cic.metasenv -> Cic.context -> Cic.term -> + Cic.term * Cic.term * CicUnification.substitution * Cic.metasenv diff --git a/helm/ocaml/cic_unification/cicUnification.mli b/helm/ocaml/cic_unification/cicUnification.mli index 46f506710..30094f7f2 100644 --- a/helm/ocaml/cic_unification/cicUnification.mli +++ b/helm/ocaml/cic_unification/cicUnification.mli @@ -61,8 +61,14 @@ val fo_unif_subst : substitution -> Cic.context -> Cic.metasenv -> Cic.term -> Cic.term -> substitution * Cic.metasenv +(* unwind_subst metasenv subst *) +(* unwinds [subst] w.r.t. itself. *) +(* It can restrict some metavariable in the [metasenv] *) +val unwind_subst : Cic.metasenv -> substitution -> substitution * Cic.metasenv + (* apply_subst subst t *) (* applies the substitution [subst] to [t] *) +(* [subst] must be already unwinded *) val apply_subst : substitution -> Cic.term -> Cic.term (* apply_subst_reducing subst (Some (mtr,reductions_no)) t *) @@ -74,5 +80,6 @@ val apply_subst : substitution -> Cic.term -> Cic.term (* eta-expansions have been performed and the head of the new *) (* application has been unified with (META [meta_to_reduce]): *) (* during the unwinding the eta-expansions are undone. *) +(* [subst] must be already unwinded *) val apply_subst_reducing : substitution -> (int * int) option -> Cic.term -> Cic.term -- 2.39.2