diff options
author | 2006-04-28 14:59:16 +0000 | |
---|---|---|
committer | 2006-04-28 14:59:16 +0000 | |
commit | 2c4a6b4efe55a2c6ca9ca7b185723e7909e57269 (patch) | |
tree | e1542c8adb83ff297284eefc23a2703461713d9b /kernel/term.ml | |
parent | 514dce2dfe717e3ed2e37dce6467b56219d451c1 (diff) | |
parent | 3ef7797ef6fc605dfafb32523261fe1b023aeecb (diff) |
Merge commit 'upstream/8.0pl3+8.1alpha' into 8.0pl3+8.1alpha
Diffstat (limited to 'kernel/term.ml')
-rw-r--r-- | kernel/term.ml | 190 |
1 files changed, 95 insertions, 95 deletions
diff --git a/kernel/term.ml b/kernel/term.ml index 30e73e4f..7060d000 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -6,9 +6,9 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: term.ml,v 1.95.2.1 2004/07/16 19:30:26 herbelin Exp $ *) +(* $Id: term.ml 8049 2006-02-16 10:42:18Z coq $ *) -(* This module instanciates the structure of generic deBruijn terms to Coq *) +(* This module instantiates the structure of generic deBruijn terms to Coq *) open Util open Pp @@ -21,6 +21,8 @@ open Esubst type existential_key = int type metavariable = int +(* This defines the strategy to use for verifiying a Cast *) + (* This defines Cases annotations *) type pattern_source = DefaultPat of int | RegularPat type case_style = LetStyle | IfStyle | MatchStyle | RegularStyle @@ -31,6 +33,7 @@ type case_printing = type case_info = { ci_ind : inductive; ci_npar : int; + ci_cstr_nargs : int array; (* number of real args of each constructor *) ci_pp_info : case_printing (* not interpreted by the kernel *) } @@ -56,6 +59,8 @@ let family_of_sort = function (* Constructions as implemented *) (********************************************************************) +type cast_kind = VMcast | DEFAULTcast + (* [constr array] is an instance matching definitional [named_context] in the same order (i.e. last argument first) *) type 'constr pexistential = existential_key * 'constr array @@ -74,7 +79,7 @@ type ('constr, 'types) kind_of_term = | Meta of metavariable | Evar of 'constr pexistential | Sort of sorts - | Cast of 'constr * 'types + | Cast of 'constr * cast_kind * 'types | Prod of name * 'types * 'types | Lambda of name * 'types * 'constr | LetIn of name * 'constr * 'types * 'constr @@ -89,14 +94,14 @@ type ('constr, 'types) kind_of_term = (* Experimental *) type ('constr, 'types) kind_of_type = | SortType of sorts - | CastType of 'types * 'types + | CastType of 'types * 'types | ProdType of name * 'types * 'types | LetInType of name * 'constr * 'types * 'types | AtomicType of 'constr * 'constr array let kind_of_type = function | Sort s -> SortType s - | Cast (c,t) -> CastType (c, t) + | Cast (c,_,t) -> CastType (c, t) | Prod (na,t,c) -> ProdType (na, t, c) | LetIn (na,b,t,c) -> LetInType (na, b, t, c) | App (c,l) -> AtomicType (c, l) @@ -123,7 +128,7 @@ let comp_term t1 t2 = | Meta m1, Meta m2 -> m1 == m2 | Var id1, Var id2 -> id1 == id2 | Sort s1, Sort s2 -> s1 == s2 - | Cast (c1,t1), Cast (c2,t2) -> c1 == c2 & t1 == t2 + | Cast (c1,_,t1), Cast (c2,_,t2) -> c1 == c2 & t1 == t2 | Prod (n1,t1,c1), Prod (n2,t2,c2) -> n1 == n2 & t1 == t2 & c1 == c2 | Lambda (n1,t1,c1), Lambda (n2,t2,c2) -> n1 == n2 & t1 == t2 & c1 == c2 | LetIn (n1,b1,t1,c1), LetIn (n2,b2,t2,c2) -> @@ -148,19 +153,19 @@ let comp_term t1 t2 = & array_for_all2 (==) bl1 bl2 | _ -> false -let hash_term (sh_rec,(sh_sort,sh_kn,sh_na,sh_id)) t = +let hash_term (sh_rec,(sh_sort,sh_con,sh_kn,sh_na,sh_id)) t = match t with | Rel _ -> t | Meta x -> Meta x | Var x -> Var (sh_id x) | Sort s -> Sort (sh_sort s) - | Cast (c,t) -> Cast (sh_rec c, sh_rec t) + | Cast (c, k, t) -> Cast (sh_rec c, k, (sh_rec t)) | Prod (na,t,c) -> Prod (sh_na na, sh_rec t, sh_rec c) | Lambda (na,t,c) -> Lambda (sh_na na, sh_rec t, sh_rec c) | LetIn (na,b,t,c) -> LetIn (sh_na na, sh_rec b, sh_rec t, sh_rec c) | App (c,l) -> App (sh_rec c, Array.map sh_rec l) | Evar (e,l) -> Evar (e, Array.map sh_rec l) - | Const c -> Const (sh_kn c) + | Const c -> Const (sh_con c) | Ind (kn,i) -> Ind (sh_kn kn,i) | Construct ((kn,i),j) -> Construct ((sh_kn kn,i),j) | Case (ci,p,c,bl) -> (* TO DO: extract ind_kn *) @@ -179,15 +184,16 @@ module Hconstr = struct type t = constr type u = (constr -> constr) * - ((sorts -> sorts) * (kernel_name -> kernel_name) - * (name -> name) * (identifier -> identifier)) + ((sorts -> sorts) * (constant -> constant) * + (kernel_name -> kernel_name) * (name -> name) * + (identifier -> identifier)) let hash_sub = hash_term let equal = comp_term let hash = Hashtbl.hash end) -let hcons_term (hsorts,hkn,hname,hident) = - Hashcons.recursive_hcons Hconstr.f (hsorts,hkn,hname,hident) +let hcons_term (hsorts,hcon,hkn,hname,hident) = + Hashcons.recursive_hcons Hconstr.f (hsorts,hcon,hkn,hname,hident) (* Constructs a DeBrujin index with number n *) let rels = @@ -206,11 +212,12 @@ let mkVar id = Var id let mkSort s = Sort s (* Constructs the term t1::t2, i.e. the term t1 casted with the type t2 *) -(* (that means t2 is declared as the type of t1) *) -let mkCast (t1,t2) = +(* (that means t2 is declared as the type of t1) + [s] is the strategy to use when *) +let mkCast (t1,k2,t2) = match t1 with - | Cast (t,_) -> Cast (t,t2) - | _ -> Cast (t1,t2) + | Cast (c,k1, _) when k1 = k2 -> Cast (c,k1,t2) + | _ -> Cast (t1,k2,t2) (* Constructs the product (x:t1)t2 *) let mkProd (x,t1,t2) = Prod (x,t1,t2) @@ -225,7 +232,7 @@ let mkLetIn (x,c1,t,c2) = LetIn (x,c1,t,c2) (* We ensure applicative terms have at least one argument and the function is not itself an applicative term *) let mkApp (f, a) = - if a=[||] then f else + if Array.length a = 0 then f else match f with | App (g, cl) -> App (g, Array.append cl a) | _ -> App (f, a) @@ -309,22 +316,22 @@ let destSort c = match kind_of_term c with let rec isprop c = match kind_of_term c with | Sort (Prop _) -> true - | Cast (c,_) -> isprop c + | Cast (c,_,_) -> isprop c | _ -> false let rec is_Prop c = match kind_of_term c with | Sort (Prop Null) -> true - | Cast (c,_) -> is_Prop c + | Cast (c,_,_) -> is_Prop c | _ -> false let rec is_Set c = match kind_of_term c with | Sort (Prop Pos) -> true - | Cast (c,_) -> is_Set c + | Cast (c,_,_) -> is_Set c | _ -> false let rec is_Type c = match kind_of_term c with | Sort (Type _) -> true - | Cast (c,_) -> is_Type c + | Cast (c,_,_) -> is_Type c | _ -> false let isType = function @@ -344,10 +351,11 @@ let isEvar c = match kind_of_term c with Evar _ -> true | _ -> false (* Destructs a casted term *) let destCast c = match kind_of_term c with - | Cast (t1, t2) -> (t1,t2) + | Cast (t1,k,t2) -> (t1,k,t2) | _ -> invalid_arg "destCast" -let isCast c = match kind_of_term c with Cast (_,_) -> true | _ -> false +let isCast c = match kind_of_term c with Cast _ -> true | _ -> false + (* Tests if a de Bruijn index *) let isRel c = match kind_of_term c with Rel _ -> true | _ -> false @@ -374,12 +382,16 @@ let destLetIn c = match kind_of_term c with | _ -> invalid_arg "destProd" (* Destructs an application *) -let destApplication c = match kind_of_term c with +let destApp c = match kind_of_term c with | App (f,a) -> (f, a) | _ -> invalid_arg "destApplication" +let destApplication = destApp + let isApp c = match kind_of_term c with App _ -> true | _ -> false +let isProd c = match kind_of_term c with | Prod(_) -> true | _ -> false + (* Destructs a constant *) let destConst c = match kind_of_term c with | Const kn -> kn @@ -423,24 +435,41 @@ let destCoFix c = match kind_of_term c with | _ -> invalid_arg "destCoFix" (******************************************************************) +(* Cast management *) +(******************************************************************) + +let rec strip_outer_cast c = match kind_of_term c with + | Cast (c,_,_) -> strip_outer_cast c + | _ -> c + +(* Fonction spéciale qui laisse les cast clés sous les Fix ou les Case *) + +let under_outer_cast f c = match kind_of_term c with + | Cast (b,k,t) -> mkCast (f b, k, f t) + | _ -> f c + +let rec under_casts f c = match kind_of_term c with + | Cast (c,k,t) -> mkCast (under_casts f c, k, t) + | _ -> f c + +(******************************************************************) (* Flattening and unflattening of embedded applications and casts *) (******************************************************************) -(* flattens application lists *) +(* flattens application lists throwing casts in-between *) let rec collapse_appl c = match kind_of_term c with | App (f,cl) -> - let rec collapse_rec f cl2 = match kind_of_term f with + let rec collapse_rec f cl2 = + match kind_of_term (strip_outer_cast f) with | App (g,cl1) -> collapse_rec g (Array.append cl1 cl2) - | Cast (c,_) when isApp c -> collapse_rec c cl2 - | _ -> if cl2 = [||] then f else mkApp (f,cl2) - in + | _ -> mkApp (f,cl2) + in collapse_rec f cl | _ -> c -let rec decompose_app c = - match kind_of_term (collapse_appl c) with +let decompose_app c = + match kind_of_term c with | App (f,cl) -> (f, Array.to_list cl) - | Cast (c,t) -> decompose_app c | _ -> (c,[]) (* strips head casts and flattens head applications *) @@ -448,11 +477,11 @@ let rec strip_head_cast c = match kind_of_term c with | App (f,cl) -> let rec collapse_rec f cl2 = match kind_of_term f with | App (g,cl1) -> collapse_rec g (Array.append cl1 cl2) - | Cast (c,_) -> collapse_rec c cl2 - | _ -> if cl2 = [||] then f else mkApp (f,cl2) + | Cast (c,_,_) -> collapse_rec c cl2 + | _ -> if Array.length cl2 = 0 then f else mkApp (f,cl2) in collapse_rec f cl - | Cast (c,t) -> strip_head_cast c + | Cast (c,_,_) -> strip_head_cast c | _ -> c (****************************************************************************) @@ -466,7 +495,7 @@ let rec strip_head_cast c = match kind_of_term c with let fold_constr f acc c = match kind_of_term c with | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ | Construct _) -> acc - | Cast (c,t) -> f (f acc c) t + | Cast (c,_,t) -> f (f acc c) t | Prod (_,t,c) -> f (f acc t) c | Lambda (_,t,c) -> f (f acc t) c | LetIn (_,b,t,c) -> f (f (f acc b) t) c @@ -487,7 +516,7 @@ let fold_constr f acc c = match kind_of_term c with let iter_constr f c = match kind_of_term c with | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ | Construct _) -> () - | Cast (c,t) -> f c; f t + | Cast (c,_,t) -> f c; f t | Prod (_,t,c) -> f t; f c | Lambda (_,t,c) -> f t; f c | LetIn (_,b,t,c) -> f b; f t; f c @@ -506,7 +535,7 @@ let iter_constr f c = match kind_of_term c with let iter_constr_with_binders g f n c = match kind_of_term c with | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ | Construct _) -> () - | Cast (c,t) -> f n c; f n t + | Cast (c,_,t) -> f n c; f n t | Prod (_,t,c) -> f n t; f (g n) c | Lambda (_,t,c) -> f n t; f (g n) c | LetIn (_,b,t,c) -> f n b; f n t; f (g n) c @@ -527,7 +556,7 @@ let iter_constr_with_binders g f n c = match kind_of_term c with let map_constr f c = match kind_of_term c with | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ | Construct _) -> c - | Cast (c,t) -> mkCast (f c, f t) + | Cast (c,k,t) -> mkCast (f c, k, f t) | Prod (na,t,c) -> mkProd (na, f t, f c) | Lambda (na,t,c) -> mkLambda (na, f t, f c) | LetIn (na,b,t,c) -> mkLetIn (na, f b, f t, f c) @@ -548,7 +577,7 @@ let map_constr f c = match kind_of_term c with let map_constr_with_binders g f l c = match kind_of_term c with | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ | Construct _) -> c - | Cast (c,t) -> mkCast (f l c, f l t) + | Cast (c,k,t) -> mkCast (f l c, k, f l t) | Prod (na,t,c) -> mkProd (na, f l t, f (g l) c) | Lambda (na,t,c) -> mkLambda (na, f l t, f (g l) c) | LetIn (na,b,t,c) -> mkLetIn (na, f l b, f l t, f (g l) c) @@ -573,8 +602,8 @@ let compare_constr f t1 t2 = | Meta m1, Meta m2 -> m1 = m2 | Var id1, Var id2 -> id1 = id2 | Sort s1, Sort s2 -> s1 = s2 - | Cast (c1,_), _ -> f c1 t2 - | _, Cast (c2,_) -> f t1 c2 + | Cast (c1,_,_), _ -> f c1 t2 + | _, Cast (c2,_,_) -> f t1 c2 | Prod (_,t1,c1), Prod (_,t2,c2) -> f t1 t2 & f c1 c2 | Lambda (_,t1,c1), Lambda (_,t2,c2) -> f t1 t2 & f c1 c2 | LetIn (_,b1,t1,c1), LetIn (_,b2,t2,c2) -> f b1 b2 & f t1 t2 & f c1 c2 @@ -605,6 +634,8 @@ let compare_constr f t1 t2 = type types = constr +type strategy = types option + let type_app f tt = f tt let body_of_type ty = ty @@ -671,7 +702,7 @@ let noccur_with_meta n m term = | Rel p -> if n<=p & p<n+m then raise LocalOccur | App(f,cl) -> (match kind_of_term f with - | Cast (c,_) when isMeta c -> () + | Cast (c,_,_) when isMeta c -> () | Meta _ -> () | _ -> iter_constr_with_binders succ occur_rec n c) | Evar (_, _) -> () @@ -746,7 +777,7 @@ let substl laml = substn_many (Array.map make_substituend (Array.of_list laml)) 0 let subst1 lam = substl [lam] -let substl_decl laml (id,bodyopt,typ as d) = +let substl_decl laml (id,bodyopt,typ) = match bodyopt with | None -> (id,None,substl laml typ) | Some body -> (id, Some (substl laml body), type_app (substl laml) typ) @@ -789,32 +820,6 @@ let substn_vars p vars = let subst_vars = substn_vars 1 -(* -map_kn : (kernel_name -> kernel_name) -> constr -> constr - -This should be rewritten to prevent duplication of constr's when not -necessary. -For now, it uses map_constr and is rather ineffective -*) - -let rec map_kn f c = - let func = map_kn f in - match kind_of_term c with - | Const kn -> - mkConst (f kn) - | Ind (kn,i) -> - mkInd (f kn,i) - | Construct ((kn,i),j) -> - mkConstruct ((f kn,i),j) - | Case (ci,p,c,l) -> - let ci' = { ci with ci_ind = let (kn,i) = ci.ci_ind in f kn, i } in - mkCase (ci', func p, func c, array_smartmap func l) - | _ -> map_constr func c - -let subst_mps sub = - map_kn (subst_kn sub) - - (*********************) (* Term constructors *) (*********************) @@ -965,20 +970,6 @@ let mkCoFix = mkCoFix let implicit_sort = Type (make_univ(make_dirpath[id_of_string"implicit"],0)) let mkImplicit = mkSort implicit_sort -let rec strip_outer_cast c = match kind_of_term c with - | Cast (c,_) -> strip_outer_cast c - | _ -> c - -(* Fonction spéciale qui laisse les cast clés sous les Fix ou les Case *) - -let under_outer_cast f c = match kind_of_term c with - | Cast (b,t) -> mkCast (f b,f t) - | _ -> f c - -let rec under_casts f c = match kind_of_term c with - | Cast (c,t) -> mkCast (under_casts f c, t) - | _ -> f c - (***************************) (* Other term constructors *) (***************************) @@ -1027,7 +1018,7 @@ let rec to_lambda n prod = else match kind_of_term prod with | Prod (na,ty,bd) -> mkLambda (na,ty,to_lambda (n-1) bd) - | Cast (c,_) -> to_lambda n c + | Cast (c,_,_) -> to_lambda n c | _ -> errorlabstrm "to_lambda" (mt ()) let rec to_prod n lam = @@ -1036,7 +1027,7 @@ let rec to_prod n lam = else match kind_of_term lam with | Lambda (na,ty,bd) -> mkProd (na,ty,to_prod (n-1) bd) - | Cast (c,_) -> to_prod n c + | Cast (c,_,_) -> to_prod n c | _ -> errorlabstrm "to_prod" (mt ()) (* pseudo-reduction rule: @@ -1066,7 +1057,7 @@ let prod_applist t nL = List.fold_left prod_app t nL let decompose_prod = let rec prodec_rec l c = match kind_of_term c with | Prod (x,t,c) -> prodec_rec ((x,t)::l) c - | Cast (c,_) -> prodec_rec l c + | Cast (c,_,_) -> prodec_rec l c | _ -> l,c in prodec_rec [] @@ -1076,7 +1067,7 @@ let decompose_prod = let decompose_lam = let rec lamdec_rec l c = match kind_of_term c with | Lambda (x,t,c) -> lamdec_rec ((x,t)::l) c - | Cast (c,_) -> lamdec_rec l c + | Cast (c,_,_) -> lamdec_rec l c | _ -> l,c in lamdec_rec [] @@ -1089,7 +1080,7 @@ let decompose_prod_n n = if n=0 then l,c else match kind_of_term c with | Prod (x,t,c) -> prodec_rec ((x,t)::l) (n-1) c - | Cast (c,_) -> prodec_rec l n c + | Cast (c,_,_) -> prodec_rec l n c | _ -> error "decompose_prod_n: not enough products" in prodec_rec [] n @@ -1102,7 +1093,7 @@ let decompose_lam_n n = if n=0 then l,c else match kind_of_term c with | Lambda (x,t,c) -> lamdec_rec ((x,t)::l) (n-1) c - | Cast (c,_) -> lamdec_rec l n c + | Cast (c,_,_) -> lamdec_rec l n c | _ -> error "decompose_lam_n: not enough abstractions" in lamdec_rec [] n @@ -1112,7 +1103,7 @@ let decompose_lam_n n = let nb_lam = let rec nbrec n c = match kind_of_term c with | Lambda (_,_,c) -> nbrec (n+1) c - | Cast (c,_) -> nbrec n c + | Cast (c,_,_) -> nbrec n c | _ -> n in nbrec 0 @@ -1121,7 +1112,7 @@ let nb_lam = let nb_prod = let rec nbrec n c = match kind_of_term c with | Prod (_,_,c) -> nbrec (n+1) c - | Cast (c,_) -> nbrec n c + | Cast (c,_,_) -> nbrec n c | _ -> n in nbrec 0 @@ -1137,6 +1128,7 @@ let nb_prod = let rec eq_constr m n = (m==n) or compare_constr eq_constr m n + let eq_constr m n = eq_constr m n (* to avoid tracing a recursive fun *) (*******************) @@ -1177,10 +1169,18 @@ module Hsorts = let hsort = Hsorts.f -let hcons_constr (hkn,hdir,hname,hident,hstr) = +let hcons_constr (hcon,hkn,hdir,hname,hident,hstr) = let hsortscci = Hashcons.simple_hcons hsort hcons1_univ in - let hcci = hcons_term (hsortscci,hkn,hname,hident) in + let hcci = hcons_term (hsortscci,hcon,hkn,hname,hident) in let htcci = Hashcons.simple_hcons Htype.f (hcci,hsortscci) in (hcci,htcci) let (hcons1_constr, hcons1_types) = hcons_constr (hcons_names()) + + +(*******) +(* Type of abstract machine values *) +type values + + + |