diff options
Diffstat (limited to 'checker/term.ml')
| -rw-r--r-- | checker/term.ml | 254 |
1 files changed, 100 insertions, 154 deletions
diff --git a/checker/term.ml b/checker/term.ml index d0d7805d..93540276 100644 --- a/checker/term.ml +++ b/checker/term.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -8,132 +8,36 @@ (* This module instantiates the structure of generic deBruijn terms to Coq *) +open Errors open Util -open Pp open Names -open Univ open Esubst -open Validate - -(* Coq abstract syntax with deBruijn variables; 'a is the type of sorts *) - -type existential_key = int -type metavariable = int - -(* This defines the strategy to use for verifiying a Cast *) - -(* This defines Cases annotations *) -type case_style = LetStyle | IfStyle | LetPatternStyle | MatchStyle | - RegularStyle -type case_printing = - { ind_nargs : int; (* length of the arity of the inductive type *) - style : case_style } -type case_info = - { ci_ind : inductive; - ci_npar : int; - ci_cstr_ndecls : int array; (* number of pattern var of each constructor *) - ci_pp_info : case_printing (* not interpreted by the kernel *) - } -let val_ci = - let val_cstyle = val_enum "case_style" 5 in - let val_cprint = val_tuple ~name:"case_printing" [|val_int;val_cstyle|] in - val_tuple ~name:"case_info" [|val_ind;val_int;val_array val_int;val_cprint|] -(* Sorts. *) - -type contents = Pos | Null - -type sorts = - | Prop of contents (* proposition types *) - | Type of universe +open Cic -type sorts_family = InProp | InSet | InType +(* Sorts. *) let family_of_sort = function | Prop Null -> InProp | Prop Pos -> InSet | Type _ -> InType -let val_sort = val_sum "sort" 0 [|[|val_enum "cnt" 2|];[|val_univ|]|] -let val_sortfam = val_enum "sorts_family" 3 +let family_equal = (==) + +let sort_of_univ u = + if Univ.is_type0m_univ u then Prop Null + else if Univ.is_type0_univ u then Prop Pos + else Type u (********************************************************************) (* Constructions as implemented *) (********************************************************************) -(* [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 -type 'constr prec_declaration = - name array * 'constr array * 'constr array -type 'constr pfixpoint = - (int array * int) * 'constr prec_declaration -type 'constr pcofixpoint = - int * 'constr prec_declaration - -let val_evar f = val_tuple ~name:"pexistential" [|val_int;val_array f|] -let val_prec f = - val_tuple ~name:"prec_declaration" - [|val_array val_name; val_array f; val_array f|] -let val_fix f = - val_tuple ~name:"pfixpoint" - [|val_tuple~name:"fix2"[|val_array val_int;val_int|];val_prec f|] -let val_cofix f = val_tuple ~name:"pcofixpoint"[|val_int;val_prec f|] - -type cast_kind = VMcast | DEFAULTcast -let val_cast = val_enum "cast_kind" 2 - -(*s*******************************************************************) -(* The type of constructions *) - -type constr = - | Rel of int - | Var of identifier - | Meta of metavariable - | Evar of constr pexistential - | Sort of sorts - | Cast of constr * cast_kind * constr - | Prod of name * constr * constr - | Lambda of name * constr * constr - | LetIn of name * constr * constr * constr - | App of constr * constr array - | Const of constant - | Ind of inductive - | Construct of constructor - | Case of case_info * constr * constr * constr array - | Fix of constr pfixpoint - | CoFix of constr pcofixpoint - -let val_constr = val_rec_sum "constr" 0 (fun val_constr -> [| - [|val_int|]; (* Rel *) - [|val_id|]; (* Var *) - [|val_int|]; (* Meta *) - [|val_evar val_constr|]; (* Evar *) - [|val_sort|]; (* Sort *) - [|val_constr;val_cast;val_constr|]; (* Cast *) - [|val_name;val_constr;val_constr|]; (* Prod *) - [|val_name;val_constr;val_constr|]; (* Lambda *) - [|val_name;val_constr;val_constr;val_constr|]; (* LetIn *) - [|val_constr;val_array val_constr|]; (* App *) - [|val_con|]; (* Const *) - [|val_ind|]; (* Ind *) - [|val_cstr|]; (* Construct *) - [|val_ci;val_constr;val_constr;val_array val_constr|]; (* Case *) - [|val_fix val_constr|]; (* Fix *) - [|val_cofix val_constr|] (* CoFix *) -|]) - -type existential = constr pexistential -type rec_declaration = constr prec_declaration -type fixpoint = constr pfixpoint -type cofixpoint = constr pcofixpoint - - let rec strip_outer_cast c = match c with | Cast (c,_,_) -> strip_outer_cast c | _ -> c -let rec collapse_appl c = match c with +let collapse_appl c = match c with | App (f,cl) -> let rec collapse_rec f cl2 = match (strip_outer_cast f) with @@ -176,6 +80,7 @@ let iter_constr_with_binders g f n c = match c with | CoFix (_,(_,tl,bl)) -> Array.iter (f n) tl; Array.iter (f (iterate g (Array.length tl) n)) bl + | Proj (p, c) -> f n c exception LocalOccur @@ -197,7 +102,7 @@ let closed0 = closedn 0 let noccurn n term = let rec occur_rec n c = match c with - | Rel m -> if m = n then raise LocalOccur + | Rel m -> if Int.equal m n then raise LocalOccur | _ -> iter_constr_with_binders succ occur_rec n c in try occur_rec n term; true with LocalOccur -> false @@ -221,7 +126,7 @@ let noccur_between n m term = let noccur_with_meta n m term = let rec occur_rec n c = match c with - | Rel p -> if n<=p & p<n+m then raise LocalOccur + | Rel p -> if n<=p && p<n+m then raise LocalOccur | App(f,cl) -> (match f with | (Cast (Meta _,_,_)| Meta _) -> () @@ -252,6 +157,7 @@ let map_constr_with_binders g f l c = match c with | CoFix(ln,(lna,tl,bl)) -> let l' = iterate g (Array.length tl) l in CoFix (ln,(lna,Array.map (f l) tl,Array.map (f l') bl)) + | Proj (p, c) -> Proj (p, f l c) (* The generic lifting function *) let rec exliftn el c = match c with @@ -291,7 +197,7 @@ let make_substituend c = { sinfo=Unknown; sit=c } let substn_many lamv n c = let lv = Array.length lamv in - if lv = 0 then c + if Int.equal lv 0 then c else let rec substrec depth c = match c with | Rel k -> @@ -311,23 +217,6 @@ let subst1 lam = substl [lam] (* Type of assumptions and contexts *) (***************************************************************************) -let val_ndecl = - val_tuple ~name:"named_declaration"[|val_id;val_opt val_constr;val_constr|] -let val_rdecl = - val_tuple ~name:"rel_declaration"[|val_name;val_opt val_constr;val_constr|] -let val_nctxt = val_list val_ndecl -let val_rctxt = val_list val_rdecl - -type named_declaration = identifier * constr option * constr -type rel_declaration = name * constr option * constr - -type named_context = named_declaration list -let empty_named_context = [] -let fold_named_context f l ~init = List.fold_right f l init - -type section_context = named_context - -type rel_context = rel_declaration list let empty_rel_context = [] let rel_context_length = List.length let rel_context_nhyps hyps = @@ -338,16 +227,14 @@ let rel_context_nhyps hyps = nhyps 0 hyps let fold_rel_context f l ~init = List.fold_right f l init -let map_context f l = +let map_rel_context f l = let map_decl (n, body_o, typ as decl) = let body_o' = Option.smartmap f body_o in let typ' = f typ in if body_o' == body_o && typ' == typ then decl else (n, body_o', typ') in - list_smartmap map_decl l - -let map_rel_context = map_context + List.smartmap map_decl l let extended_rel_list n hyps = let rec reln l p = function @@ -383,7 +270,7 @@ let decompose_lam_n_assum n = if n < 0 then error "decompose_lam_n_assum: integer parameter must be positive"; let rec lamdec_rec l n c = - if n=0 then l,c + if Int.equal n 0 then l,c else match c with | Lambda (x,t,c) -> lamdec_rec ((x,None,t) :: l) (n-1) c | LetIn (x,b,t,c) -> lamdec_rec ((x,Some b,t) :: l) n c @@ -416,7 +303,7 @@ let decompose_prod_n_assum n = if n < 0 then error "decompose_prod_n_assum: integer parameter must be positive"; let rec prodec_rec l n c = - if n=0 then l,c + if Int.equal n 0 then l,c else match c with | Prod (x,t,c) -> prodec_rec ((x,None,t) :: l) (n-1) c | LetIn (x,b,t,c) -> prodec_rec ((x,Some b,t) :: l) (n-1) c @@ -441,7 +328,7 @@ let destArity = | LetIn (x,b,t,c) -> prodec_rec ((x,Some b,t)::l) c | Cast (c,_,_) -> prodec_rec l c | Sort s -> l,s - | _ -> anomaly "destArity: not an arity" + | _ -> anomaly ~label:"destArity" (Pp.str "not an arity") in prodec_rec [] @@ -459,40 +346,99 @@ let rec isArity c = (* alpha conversion : ignore print names and casts *) +let compare_sorts s1 s2 = match s1, s2 with +| Prop c1, Prop c2 -> + begin match c1, c2 with + | Pos, Pos | Null, Null -> true + | Pos, Null -> false + | Null, Pos -> false + end +| Type u1, Type u2 -> Univ.Universe.equal u1 u2 +| Prop _, Type _ -> false +| Type _, Prop _ -> false + +let eq_puniverses f (c1,u1) (c2,u2) = + Univ.Instance.equal u1 u2 && f c1 c2 + let compare_constr f t1 t2 = match t1, t2 with - | Rel n1, Rel n2 -> n1 = n2 - | Meta m1, Meta m2 -> m1 = m2 - | Var id1, Var id2 -> id1 = id2 - | Sort s1, Sort s2 -> s1 = s2 + | Rel n1, Rel n2 -> Int.equal n1 n2 + | Meta m1, Meta m2 -> Int.equal m1 m2 + | Var id1, Var id2 -> Id.equal id1 id2 + | Sort s1, Sort s2 -> compare_sorts s1 s2 | 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 + | 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 | App (c1,l1), App (c2,l2) -> - if Array.length l1 = Array.length l2 then - f c1 c2 & array_for_all2 f l1 l2 + if Int.equal (Array.length l1) (Array.length l2) then + f c1 c2 && Array.for_all2 f l1 l2 else let (h1,l1) = decompose_app t1 in let (h2,l2) = decompose_app t2 in - if List.length l1 = List.length l2 then - f h1 h2 & List.for_all2 f l1 l2 + if Int.equal (List.length l1) (List.length l2) then + f h1 h2 && List.for_all2 f l1 l2 else false - | Evar (e1,l1), Evar (e2,l2) -> e1 = e2 & array_for_all2 f l1 l2 - | Const c1, Const c2 -> eq_con_chk c1 c2 - | Ind c1, Ind c2 -> eq_ind_chk c1 c2 - | Construct (c1,i1), Construct (c2,i2) -> i1=i2 && eq_ind_chk c1 c2 + | Evar (e1,l1), Evar (e2,l2) -> Int.equal e1 e2 && Array.equal f l1 l2 + | Const c1, Const c2 -> eq_puniverses eq_con_chk c1 c2 + | Ind c1, Ind c2 -> eq_puniverses eq_ind_chk c1 c2 + | Construct ((c1,i1),u1), Construct ((c2,i2),u2) -> Int.equal i1 i2 && eq_ind_chk c1 c2 + && Univ.Instance.equal u1 u2 | Case (_,p1,c1,bl1), Case (_,p2,c2,bl2) -> - f p1 p2 & f c1 c2 & array_for_all2 f bl1 bl2 - | Fix (ln1,(_,tl1,bl1)), Fix (ln2,(_,tl2,bl2)) -> - ln1 = ln2 & array_for_all2 f tl1 tl2 & array_for_all2 f bl1 bl2 + f p1 p2 && f c1 c2 && Array.equal f bl1 bl2 + | Fix ((ln1, i1),(_,tl1,bl1)), Fix ((ln2, i2),(_,tl2,bl2)) -> + Int.equal i1 i2 && Array.equal Int.equal ln1 ln2 && + Array.equal f tl1 tl2 && Array.equal f bl1 bl2 | CoFix(ln1,(_,tl1,bl1)), CoFix(ln2,(_,tl2,bl2)) -> - ln1 = ln2 & array_for_all2 f tl1 tl2 & array_for_all2 f bl1 bl2 + Int.equal ln1 ln2 && Array.equal f tl1 tl2 && Array.equal f bl1 bl2 + | Proj (p1,c1), Proj(p2,c2) -> eq_con_chk p1 p2 && f c1 c2 | _ -> false let rec eq_constr m n = - (m==n) or + (m == n) || compare_constr eq_constr m n let eq_constr m n = eq_constr m n (* to avoid tracing a recursive fun *) + +(* Universe substitutions *) + +let map_constr f c = map_constr_with_binders (fun x -> x) (fun _ c -> f c) 0 c + +let subst_instance_constr subst c = + if Univ.Instance.is_empty subst then c + else + let f u = Univ.subst_instance_instance subst u in + let changed = ref false in + let rec aux t = + match t with + | Const (c, u) -> + if Univ.Instance.is_empty u then t + else + let u' = f u in + if u' == u then t + else (changed := true; Const (c, u')) + | Ind (i, u) -> + if Univ.Instance.is_empty u then t + else + let u' = f u in + if u' == u then t + else (changed := true; Ind (i, u')) + | Construct (c, u) -> + if Univ.Instance.is_empty u then t + else + let u' = f u in + if u' == u then t + else (changed := true; Construct (c, u')) + | Sort (Type u) -> + let u' = Univ.subst_instance_universe subst u in + if u' == u then t else + (changed := true; Sort (sort_of_univ u')) + | _ -> map_constr aux t + in + let c' = aux c in + if !changed then c' else c + +let subst_instance_context s ctx = + if Univ.Instance.is_empty s then ctx + else map_rel_context (fun x -> subst_instance_constr s x) ctx |