From 4490dfcb94057dd6518963a904565e3a4a354bac Mon Sep 17 00:00:00 2001 From: ppedrot Date: Mon, 29 Apr 2013 16:02:05 +0000 Subject: Splitting Term into five unrelated interfaces: 1. sorts.ml: A small file utility for sorts; 2. constr.ml: Really low-level terms, essentially kind_of_constr, smart constructor and basic operators; 3. vars.ml: Everything related to term variables, that is, occurences and substitution; 4. context.ml: Rel/Named context and all that; 5. term.ml: derived utility operations on terms; also includes constr.ml up to some renaming, and acts as a compatibility layer, to be deprecated. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16462 85f007b7-540e-0410-9357-904b9bb8a0f7 --- plugins/xml/cic2acic.ml | 12 +++++++----- plugins/xml/doubleTypeInference.ml | 7 ++++--- 2 files changed, 11 insertions(+), 8 deletions(-) (limited to 'plugins/xml') diff --git a/plugins/xml/cic2acic.ml b/plugins/xml/cic2acic.ml index 98c485dba..a7a181aa6 100644 --- a/plugins/xml/cic2acic.ml +++ b/plugins/xml/cic2acic.ml @@ -170,6 +170,7 @@ let family_of_term ty = module CPropRetyping = struct module T = Term + module V = Vars let outsort env sigma t = family_of_term (DoubleTypeInference.whd_betadeltaiotacprop env sigma t) @@ -178,7 +179,7 @@ module CPropRetyping = | [] -> typ | h::rest -> match T.kind_of_term (DoubleTypeInference.whd_betadeltaiotacprop env sigma typ) with - | T.Prod (na,c1,c2) -> subst_type env sigma (T.subst1 h c2) rest + | T.Prod (na,c1,c2) -> subst_type env sigma (V.subst1 h c2) rest | _ -> Errors.anomaly (Pp.str "Non-functional construction") @@ -198,7 +199,7 @@ let typeur sigma metamap = with Not_found -> Errors.anomaly ~label:"type_of" (Pp.str "this is not a well-typed term")) | T.Rel n -> let (_,_,ty) = Environ.lookup_rel n env in - T.lift n ty + V.lift n ty | T.Var id -> (try let (_,_,ty) = Environ.lookup_named id env in @@ -222,7 +223,7 @@ let typeur sigma metamap = | T.Lambda (name,c1,c2) -> T.mkProd (name, c1, type_of (Environ.push_rel (name,None,c1) env) c2) | T.LetIn (name,b,c1,c2) -> - T.subst1 b (type_of (Environ.push_rel (name,Some b,c1) env) c2) + V.subst1 b (type_of (Environ.push_rel (name,Some b,c1) env) c2) | T.Fix ((_,i),(_,tys,_)) -> tys.(i) | T.CoFix (i,(_,tys,_)) -> tys.(i) | T.App(f,args)-> @@ -326,6 +327,7 @@ let acic_of_cic_context' computeinnertypes seed ids_to_terms constr_to_ids let module N = Names in let module A = Acic in let module T = Term in + let module V = Vars in let fresh_id' = fresh_id seed ids_to_terms constr_to_ids ids_to_father_ids in (* CSC: do you have any reasonable substitute for 503? *) let terms_to_types = Acic.CicHash.create 503 in @@ -473,7 +475,7 @@ print_endline "PASSATO" ; flush stdout ; in let eta_expanded = let arguments = - List.map (T.lift uninst_vars_length) t @ + List.map (V.lift uninst_vars_length) t @ Termops.rel_list 0 uninst_vars_length in Unshare.unshare @@ -528,7 +530,7 @@ print_endline "PASSATO" ; flush stdout ; match n with N.Anonymous -> N.Anonymous | _ -> - if not fake_dependent_products && T.noccurn 1 t then + if not fake_dependent_products && V.noccurn 1 t then N.Anonymous else N.Name diff --git a/plugins/xml/doubleTypeInference.ml b/plugins/xml/doubleTypeInference.ml index c95cf94b6..5a3880b01 100644 --- a/plugins/xml/doubleTypeInference.ml +++ b/plugins/xml/doubleTypeInference.ml @@ -59,6 +59,7 @@ let double_type_of env sigma cstr expectedty subterms_to_types = (*CSC: functions used do checks that we do not need *) let rec execute env sigma cstr expectedty = let module T = Term in + let module V = Vars in let module E = Environ in (* the type part is the synthesized type *) let judgement = @@ -84,7 +85,7 @@ let double_type_of env sigma cstr expectedty subterms_to_types = (function (m,bo,ty) -> (* Warning: the substitution should be performed also on bo *) (* This is not done since bo is not used later yet *) - (m,bo,Unshare.unshare (T.replace_vars [n,he1] ty)) + (m,bo,Unshare.unshare (V.replace_vars [n,he1] ty)) ) tl2 in iter tl1 tl2' @@ -161,7 +162,7 @@ let double_type_of env sigma cstr expectedty subterms_to_types = match T.kind_of_term (Reduction.whd_betadeltaiota env typ) with T.Prod (_,c1,c2) -> (Some (Reductionops.nf_beta sigma c1)) :: - (aux (T.subst1 hj c2) restjl) + (aux (V.subst1 hj c2) restjl) | _ -> assert false in Array.of_list (aux j.Environ.uj_type (Array.to_list args)) @@ -249,7 +250,7 @@ if Acic.CicHash.mem subterms_to_types cstr then let lara = Array.map (assumption_of_judgment env sigma) larj in let env1 = Environ.push_rec_types (names,lara,vdef) env in let expectedtypes = - Array.map (function i -> Some (Term.lift length i)) lar + Array.map (function i -> Some (Vars.lift length i)) lar in let vdefj = execute_array env1 sigma vdef expectedtypes in let vdefv = Array.map Environ.j_val vdefj in -- cgit v1.2.3