diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/environ.mli | 20 | ||||
| -rw-r--r-- | kernel/evd.ml | 64 | ||||
| -rw-r--r-- | kernel/evd.mli | 37 | ||||
| -rw-r--r-- | kernel/generic.ml | 604 | ||||
| -rw-r--r-- | kernel/generic.mli | 116 | ||||
| -rw-r--r-- | kernel/names.ml | 13 | ||||
| -rw-r--r-- | kernel/names.mli | 3 | ||||
| -rw-r--r-- | kernel/sign.ml | 28 | ||||
| -rw-r--r-- | kernel/sign.mli | 12 | ||||
| -rw-r--r-- | kernel/term.ml | 1489 | ||||
| -rw-r--r-- | kernel/term.mli | 520 | ||||
| -rw-r--r-- | kernel/univ.mli | 12 |
12 files changed, 2918 insertions, 0 deletions
diff --git a/kernel/environ.mli b/kernel/environ.mli new file mode 100644 index 0000000000..24cd002826 --- /dev/null +++ b/kernel/environ.mli @@ -0,0 +1,20 @@ + +(* $Id$ *) + +open Names +open Term +open Constant +open Inductive + +type unsafe_env + +val push_var : identifier * constr -> unsafe_env -> unsafe_env +val push_rel : name * constr -> unsafe_env -> unsafe_env + +val add_constant : constant -> unsafe_env -> unsafe_env +val add_mind : mind -> unsafe_env -> unsafe_env + + +val lookup_var : identifier -> unsafe_env -> constr +val loopup_rel : int -> unsafe_env -> name * constr + diff --git a/kernel/evd.ml b/kernel/evd.ml new file mode 100644 index 0000000000..77351ab9b7 --- /dev/null +++ b/kernel/evd.ml @@ -0,0 +1,64 @@ + +(* $Id$ *) + +open Util +open Names +open Term +open Sign + +(* The type of mappings for existential variables *) + +type evar_body = + EVAR_EMPTY | EVAR_DEFINED of constr + +type 'a evar_info = { + concl : constr; (* the type of the evar ... *) + hyps : context; (* ... under a certain signature *) + body : evar_body; (* its definition *) + info : 'a option (* any other necessary information *) +} + +type 'a evar_map = 'a evar_info Spmap.t + +let mt_evd = Spmap.empty + +let toList evc = Spmap.fold (fun sp x acc -> (sp,x)::acc) evc [] +let dom evc = Spmap.fold (fun sp _ acc -> sp::acc) evc [] +let map evc k = Spmap.find k evc +let rmv evc k = Spmap.remove k evc +let remap evc k i = Spmap.add k i evc +let in_dom evc k = Spmap.mem k evc + +let add_with_info evd sp newinfo = + Spmap.add sp newinfo evd + +let add_noinfo evd sp sign typ = + let newinfo = + { concl = typ; + hyps = sign; + body = EVAR_EMPTY; + info = None} + in + Spmap.add sp newinfo evd + +let define evd sp body = + let oldinfo = map evd sp in + let newinfo = + { concl = oldinfo.concl; + hyps = oldinfo.hyps; + body = EVAR_DEFINED body; + info = oldinfo.info} + in + match oldinfo.body with + | EVAR_EMPTY -> Spmap.add sp newinfo evd + | _ -> anomaly "cannot define an isevar twice" + +(* The list of non-instantiated existential declarations *) + +let non_instantiated sigma = + let listsp = toList sigma in + List.fold_left + (fun l ((sp,evd) as d) -> if evd.body = EVAR_EMPTY then (d::l) else l) + [] listsp + +let is_evar sigma sp = in_dom sigma sp diff --git a/kernel/evd.mli b/kernel/evd.mli new file mode 100644 index 0000000000..cb606941c0 --- /dev/null +++ b/kernel/evd.mli @@ -0,0 +1,37 @@ + +(* $Id$ *) + +open Names +open Term +open Sign + +(* The type of mappings for existential variables *) + +type evar_body = + | EVAR_EMPTY + | EVAR_DEFINED of constr + +type 'a evar_info = { + concl : constr; (* the type of the evar ... *) + hyps : context; (* ... under a certain signature *) + body : evar_body; (* its definition *) + info : 'a option (* any other possible information necessary *) +} + +type 'a evar_map + +val dom : 'c evar_map -> section_path list +val map : 'c evar_map -> section_path -> 'c evar_info +val rmv : 'c evar_map -> section_path -> 'c evar_map +val remap : 'c evar_map -> section_path -> 'c evar_info -> 'c evar_map +val in_dom : 'c evar_map -> section_path -> bool +val toList : 'c evar_map -> (section_path * 'c evar_info) list + +val mt_evd : 'c evar_map +val add_with_info : 'a evar_map -> section_path -> 'a evar_info -> 'a evar_map +val add_noinfo : 'a evar_map -> section_path -> context -> + constr -> 'a evar_map +val define : 'a evar_map -> section_path -> constr -> 'a evar_map + +val non_instantiated : 'a evar_map -> (section_path * 'a evar_info) list +val is_evar : 'a evar_map -> section_path -> bool diff --git a/kernel/generic.ml b/kernel/generic.ml new file mode 100644 index 0000000000..9adc53ce68 --- /dev/null +++ b/kernel/generic.ml @@ -0,0 +1,604 @@ + +(* $Id$ *) + +open Util +open Pp +open Names + +(********************************************************************) +(* Generic syntax of terms with de Bruijn indexes *) +(********************************************************************) + +type 'oper term = + | DOP0 of 'oper (* atomic terms *) + | DOP1 of 'oper * 'oper term (* operator of arity 1 *) + | DOP2 of 'oper * 'oper term * 'oper term (* operator of arity 2 *) + | DOPN of 'oper * 'oper term array (* operator of variadic arity *) + | DOPL of 'oper * 'oper term list (* operator of variadic arity *) + | DLAM of name * 'oper term (* deBruijn binder on one term*) + | DLAMV of name * 'oper term array (* deBruijn binder on many terms*) + | VAR of identifier (* named variable *) + | Rel of int (* variable as deBruijn index *) + +exception FreeVar +exception Occur + +let isRel = function Rel _ -> true | _ -> false +let isVAR = function VAR _ -> true | _ -> false + +(* returns the list of free debruijn indices in a term *) + +let free_rels m = + let rec frec depth acc = function + | Rel n -> if n >= depth then Intset.add (n-depth+1) acc else acc + | DOPN(_,cl) -> Array.fold_left (frec depth) acc cl + | DOPL(_,cl) -> List.fold_left (frec depth) acc cl + | DOP2(_,c1,c2) -> frec depth (frec depth acc c1) c2 + | DOP1(_,c) -> frec depth acc c + | DLAM(_,c) -> frec (depth+1) acc c + | DLAMV(_,cl) -> Array.fold_left (frec (depth+1)) acc cl + | VAR _ -> acc + | DOP0 _ -> acc + in + frec 1 Intset.empty m + +(* (closedn n M) raises FreeVar if a variable of height greater than n + occurs in M, returns () otherwise *) + +let closedn = + let rec closed_rec n = function + | Rel(m) -> if m>n then raise FreeVar + | VAR _ -> () + | DOPN(_,cl) -> Array.iter (closed_rec n) cl + | DOPL(_,cl) -> List.iter (closed_rec n) cl + | DOP2(_,c1,c2) -> closed_rec n c1; closed_rec n c2 + | DOP1(_,c) -> closed_rec n c + | DLAM(_,c) -> closed_rec (n+1) c + | DLAMV(_,v) -> Array.iter (closed_rec (n+1)) v + | _ -> () + in + closed_rec + +(* (closed M) is true iff M is a (deBruijn) closed term *) + +let closed0 term = + try closedn 0 term; true with FreeVar -> false + +(* (noccurn n M) returns true iff (Rel n) does NOT occur in term M *) + +let noccurn n term = + let rec occur_rec n = function + | Rel(m) -> if m = n then raise Occur + | VAR _ -> () + | DOPN(_,cl) -> Array.iter (occur_rec n) cl + | DOPL(_,cl) -> List.iter (occur_rec n) cl + | DOP1(_,c) -> occur_rec n c + | DOP2(_,c1,c2) -> occur_rec n c1; occur_rec n c2 + | DLAM(_,c) -> occur_rec (n+1) c + | DLAMV(_,v) -> Array.iter (occur_rec (n+1)) v + | _ -> () + in + try occur_rec n term; true with Occur -> false + +(* (noccur_bet n m M) returns true iff (Rel p) does NOT occur in term M + for n <= p < n+m *) + +let noccur_bet n m term = + let rec occur_rec n = function + | Rel(p) -> if n<=p && p<n+m then raise Occur + | VAR _ -> () + | DOPN(_,cl) -> Array.iter (occur_rec n) cl + | DOPL(_,cl) -> List.iter (occur_rec n) cl + | DOP1(_,c) -> occur_rec n c + | DOP2(_,c1,c2) -> occur_rec n c1; occur_rec n c2 + | DLAM(_,c) -> occur_rec (n+1) c + | DLAMV(_,v) -> Array.iter (occur_rec (n+1)) v + | _ -> () + in + try occur_rec n term; true with Occur -> false + +(* Explicit lifts and basic operations *) +type lift_spec = + | ELID + | ELSHFT of lift_spec * int (* ELSHFT(l,n) == lift of n, then apply lift l *) + | ELLFT of int * lift_spec (* ELLFT(n,l) == apply l to de Bruijn > n *) + (* i.e under n binders *) + +(* compose a relocation of magnitude n *) +let rec el_shft n = function + | ELSHFT(el,k) -> el_shft (k+n) el + | el -> if n = 0 then el else ELSHFT(el,n) + + +(* cross n binders *) +let rec el_liftn n = function + | ELID -> ELID + | ELLFT(k,el) -> el_liftn (n+k) el + | el -> if n=0 then el else ELLFT(n, el) + +let el_lift el = el_liftn 1 el + +(* relocation of de Bruijn n in an explicit lift *) +let rec reloc_rel n = function + | ELID -> n + | ELLFT(k,el) -> + if n <= k then n else (reloc_rel (n-k) el) + k + | ELSHFT(el,k) -> (reloc_rel (n+k) el) + + +(* The generic lifting function *) +let rec exliftn el = function + | Rel i -> Rel(reloc_rel i el) + | DOPN(oper,cl) -> DOPN(oper, Array.map (exliftn el) cl) + | DOPL(oper,cl) -> DOPL(oper, List.map (exliftn el) cl) + | DOP1(oper,c) -> DOP1(oper, exliftn el c) + | DOP2(oper,c1,c2) -> DOP2(oper, exliftn el c1, exliftn el c2) + | DLAM(na,c) -> DLAM(na, exliftn (el_lift el) c) + | DLAMV(na,v) -> DLAMV(na, Array.map (exliftn (el_lift el)) v) + | x -> x + + +(* Lifting the binding depth across k bindings *) + +let liftn k n = + match el_liftn (pred n) (el_shft k ELID) with + | ELID -> (fun c -> c) + | el -> exliftn el + +let lift k = liftn k 1 +let lift1 c = exliftn (ELSHFT(ELID,1)) c + + +(* explicit substitutions of type 'a *) +type 'a subs = + | ESID (* ESID = identity *) + | CONS of 'a * 'a subs (* CONS(t,S) = (S.t) parallel substitution *) + | SHIFT of int * 'a subs (* SHIFT(n,S) = (^n o S) terms in S are relocated *) + (* with n vars *) + | LIFT of int * 'a subs (* LIFT(n,S) = (%n S) stands for ((^n o S).n...1) *) + +(* operations of subs: collapses constructors when possible. + * Needn't be recursive if we always use these functions + *) +let subs_cons(x,s) = CONS(x,s) + +let subs_lift = function + | ESID -> ESID (* the identity lifted is still the identity *) + (* (because (^1.1) --> id) *) + | LIFT (n,lenv) -> LIFT (n+1, lenv) + | lenv -> LIFT (1,lenv) + +let subs_shft = function + | (0, s) -> s + | (n, SHIFT (k,s1)) -> SHIFT (k+n, s1) + | (n, s) -> SHIFT (n,s) + + +(* Expands de Bruijn k in the explicit substitution subs + * lams accumulates de shifts to perform when retrieving the i-th value + * the rules used are the following: + * + * [id]k --> k + * [S.t]1 --> t + * [S.t]k --> [S](k-1) if k > 1 + * [^n o S] k --> [^n]([S]k) + * [(%n S)] k --> k if k <= n + * [(%n S)] k --> [^n]([S](k-n)) + * + * the result is (Inr k) when the variable is just relocated + *) +let rec exp_rel lams k subs = + match (k,subs) with + | (1, CONS (def,_)) -> Inl(lams,def) + | (_, CONS (_,l)) -> exp_rel lams (pred k) l + | (_, LIFT (n,_)) when k<=n -> Inr(lams+k) + | (_, LIFT (n,l)) -> exp_rel (n+lams) (k-n) l + | (_, SHIFT (n,s)) -> exp_rel (n+lams) k s + | (_, ESID) -> Inr(lams+k) + +let expand_rel k subs = exp_rel 0 k subs + + +(* (subst1 M c) substitutes M for Rel(1) in c + we generalise it to (substl [M1,...,Mn] c) which substitutes in parallel + M1,...,Mn for respectively Rel(1),...,Rel(n) in c *) + +(* 1st : general case *) + +type info = Closed | Open | Unknown +type 'a substituend = { mutable sinfo: info; sit: 'a } + +let rec lift_substituend depth s = + match s.sinfo with + | Closed -> s.sit + | Open -> lift depth s.sit + | Unknown -> + s.sinfo <- if closed0 s.sit then Closed else Open; + lift_substituend depth s + +let make_substituend c = { sinfo=Unknown; sit=c } + +let substn_many lamv n = + let lv = Array.length lamv in + let rec substrec depth = function + | Rel k as x -> + if k<=depth then + x + else if k-depth <= lv then + lift_substituend depth lamv.(k-depth-1) + else + Rel (k-lv) + | VAR id -> VAR id + | DOPN(oper,cl) -> DOPN(oper,Array.map (substrec depth) cl) + | DOPL(oper,cl) -> DOPL(oper,List.map (substrec depth) cl) + | DOP1(oper,c) -> DOP1(oper,substrec depth c) + | DOP2(oper,c1,c2) -> DOP2(oper,substrec depth c1,substrec depth c2) + | DLAM(na,c) -> DLAM(na,substrec (depth+1) c) + | DLAMV(na,v) -> DLAMV(na,Array.map (substrec (depth+1)) v) + | x -> x + in + substrec n + +let substl laml = + substn_many (Array.map make_substituend (Array.of_list laml)) 0 +let subst1 lam = substl [lam] +let pop t = lift (-1) t + + +(* Various occurs checks *) + +let occur_opern s = + let rec occur_rec = function + | DOPN(oper,cl) -> s=oper or (array_exists occur_rec cl) + | DOPL(oper,cl) -> s=oper or (List.exists occur_rec cl) + | VAR _ -> false + | DOP1(_,c) -> occur_rec c + | DOP2(_,c1,c2) -> (occur_rec c1) or (occur_rec c2) + | DLAM(_,c) -> occur_rec c + | DLAMV(_,v) -> array_exists occur_rec v + | _ -> false + in + occur_rec + +let occur_oper0 s = + let rec occur_rec = function + | DOPN(_,cl) -> (array_exists occur_rec cl) + | DOPL(_,cl) -> (List.exists occur_rec cl) + | DOP0 oper -> s=oper + | VAR _ -> false + | DOP1(_,c) -> occur_rec c + | DOP2(_,c1,c2) -> (occur_rec c1) or (occur_rec c2) + | DLAM(_,c) -> occur_rec c + | DLAMV(_,v) -> array_exists occur_rec v + | _ -> false + in + occur_rec + +let occur_var s = + let rec occur_rec = function + | DOPN(_,cl) -> array_exists occur_rec cl + | DOPL(_,cl) -> List.exists occur_rec cl + | VAR id -> s=id + | DOP1(_,c) -> occur_rec c + | DOP2(_,c1,c2) -> (occur_rec c1) or (occur_rec c2) + | DLAM(_,c) -> occur_rec c + | DLAMV(_,v) -> array_exists occur_rec v + | _ -> false + in + occur_rec + +let occur_oper s = + let rec occur_rec = function + | DOPN(oper,cl) -> s=oper or (array_exists occur_rec cl) + | DOPL(oper,cl) -> s=oper or (List.exists occur_rec cl) + | VAR _ -> false + | DOP0 oper -> s=oper + | DOP1(oper,c) -> s=oper or occur_rec c + | DOP2(oper,c1,c2) -> s=oper or (occur_rec c1) or (occur_rec c2) + | DLAM(_,c) -> occur_rec c + | DLAMV(_,v) -> array_exists occur_rec v + | _ -> false + in + occur_rec + +(* Returns the list of global variables in a term *) + +let global_varsl l constr = + let rec filtrec acc = function + | VAR id -> id::acc + | DOP1(oper,c) -> filtrec acc c + | DOP2(oper,c1,c2) -> filtrec (filtrec acc c1) c2 + | DOPN(oper,cl) -> Array.fold_left filtrec acc cl + | DOPL(oper,cl) -> List.fold_left filtrec acc cl + | DLAM(_,c) -> filtrec acc c + | DLAMV(_,v) -> Array.fold_left filtrec acc v + | _ -> acc + in + filtrec l constr + +let global_vars constr = global_varsl [] constr + +let global_vars_set constr = + List.fold_left (fun s x -> Idset.add x s) Idset.empty (global_vars constr) + +(* alpha equality for generic terms : checks first if M and M' are equal, + otherwise checks equality forgetting the name annotation of DLAM and DLAMV*) + +let rec eq_term m m' = + (m == m') + or (m = m') + or (match (m,m') with + | (DOP1(oper1,c1),DOP1(oper2,c2)) -> + oper1 = oper2 & eq_term c1 c2 + | (DOP2(oper1,c1,t1),DOP2(oper2,c2,t2)) -> + oper1 = oper2 & eq_term c1 c2 & eq_term t1 t2 + | (DOPN(oper1,cl1),DOPN(oper2,cl2)) -> + oper1 = oper2 & array_for_all2 eq_term cl1 cl2 + | (DOPL(oper1,cl1),DOPL(oper2,cl2)) -> + oper1 = oper2 & List.for_all2 eq_term cl1 cl2 + | (DLAM(_,c1),DLAM(_,c2)) -> eq_term c1 c2 + | (DLAMV(_,cl1),DLAMV(_,cl2)) -> array_for_all2 eq_term cl1 cl2 + | _ -> false) + +(* (dependent M N) is true iff M is eq_term with a subterm of N + M is appropriately lifted through abstractions of N *) +let dependent = + let rec deprec m = function t -> + (eq_term m t) + or (match t with + | VAR _ -> false + | DOP1(_,c) -> deprec m c + | DOP2(_,c,t) -> deprec m c or deprec m t + | DOPN(_,cl) -> array_exists (deprec m) cl + | DOPL(_,cl) -> List.exists (deprec m) cl + | DLAM(_,c) -> deprec (lift1 m) c + | DLAMV(_,v) -> array_exists (deprec (lift1 m)) v + | _ -> false) + in + deprec + +(* (thin_val sigma) removes identity substitutions from sigma *) + +let rec thin_val = function + | [] -> [] + | (((id,{sit=VAR id'}) as s)::tl) -> + if id = id' then thin_val tl else s::(thin_val tl) + | h::tl -> h::(thin_val tl) + +(* (replace_vars sigma M) applies substitution sigma to term M *) +let replace_vars var_alist = + let var_alist = thin_val var_alist in + let rec substrec n = function + | (VAR(x) as c) -> + (try lift_substituend n (List.assoc x var_alist) + with Not_found -> c) + + | DOPN(oper,cl) -> DOPN(oper,Array.map (substrec n) cl) + | DOPL(oper,cl) -> DOPL(oper,List.map (substrec n) cl) + | DOP1(oper,c) -> DOP1(oper,substrec n c) + | DOP2(oper,c1,c2) -> DOP2(oper,substrec n c1,substrec n c2) + | DLAM(na,c) -> DLAM(na,substrec (n+1) c) + | DLAMV(na,v) -> DLAMV(na,Array.map (substrec (n+1)) v) + | x -> x + in + if var_alist = [] then (function x -> x) else substrec 0 + +let subst_varn str n = replace_vars [(str,make_substituend (Rel n))] + +(* (subst_var str t) substitute (VAR str) by (Rel 1) in t *) +let subst_var str = subst_varn str 1 + + +(* renames different ocurrences of (VAR id) in t with a fresh identifier + wrt. acc *) +let rename_diff_occ id acc t = + let rec rename_occ acc = function + | (VAR(x) as c) -> + if x <> id then + acc,c + else + let nid = next_ident_away id acc in (nid::acc), (VAR nid) + | DOPN(oper,cl) -> + let nacc,ncl = vrename_occ acc cl in nacc,DOPN(oper, ncl) + | DOPL(oper,cl) -> + let nacc,ncl = lrename_occ acc cl in nacc, DOPL(oper,ncl) + | DOP1(oper,c) -> + let nacc,nc = rename_occ acc c in nacc, DOP1(oper,nc) + | DOP2(oper,c1,c2) -> + let nacc,nc1 = rename_occ acc c1 in + let nacc2,nc2 = rename_occ nacc c2 in + nacc2, DOP2(oper,nc1,nc2) + | DLAM(na,c) -> + let nacc,nc = rename_occ acc c in (nacc, DLAM(na,nc)) + | DLAMV(na,v) -> + let nacc,nv = vrename_occ acc v in (nacc, DLAMV(na, nv)) + | x -> acc,x + and lrename_occ acc = function + | [] -> acc,[] + | (t::lt) -> + let nacc,nt = rename_occ acc t in + let nacc2,nlt = lrename_occ nacc lt + in nacc2,(nt::nlt) + and vrename_occ acc v = + let nacc,nl = lrename_occ acc (Array.to_list v) + in nacc, Array.of_list nl + in + rename_occ acc t + + +let sAPP c n = + match c with + | DLAM(na,m) -> subst1 n m + | _ -> invalid_arg "SAPP" + +let sAPPV c n = + match c with + | DLAMV(na,mV) -> Array.map (subst1 n) mV + | _ -> invalid_arg "SAPPV" + +let sAPPVi i c n = + match c with + | DLAMV(na,mV) -> subst1 n mV.(i) + | _ -> invalid_arg "SAPPVi" + +let sAPPList constr cl = + let rec srec stack = function + | (DLAM(_,c), (h::t)) -> srec (h::stack) (c,t) + | (c, []) -> substl stack c + | (_, _) -> failwith "SAPPList" + in + srec [] (constr,cl) + +let sAPPVList constr cl = + let rec srec stack = function + | (DLAM(_,c), (h::t)) -> srec (h::stack) (c,t) + | (DLAMV(_,c), [h]) -> Array.map (substl (h::stack)) c + | (_, _) -> failwith "SAPPVList" + in + srec [] (constr,cl) + +let sAPPViList i constr cl= + let rec srec stack = function + | (DLAM(_,c), (h::t)) -> srec (h::stack) (c,t) + | (DLAMV(_,c), [h]) -> substl (h::stack) c.(i) + | (_, _) -> failwith "SAPPViList" + in + srec [] (constr,cl) + +let under_dlams f = + let rec apprec = function + | DLAMV(na,c) -> DLAMV(na,Array.map f c) + | DLAM(na,c) -> DLAM(na,apprec c) + | _ -> failwith "under_dlams" + in + apprec + + +(* utility for discharge *) +type modification_action = ABSTRACT | ERASE + +let interp_modif absfun oper (oper',modif) cl = + let rec interprec = function + | ([], cl) -> DOPN(oper',Array.of_list cl) + | (ERASE::tlm, c::cl) -> interprec (tlm,cl) + | (ABSTRACT::tlm, c::cl) -> absfun (interprec (tlm,cl)) c + | _ -> assert false + in + interprec (modif,cl) + + +type 'a modification = + | NOT_OCCUR + | DO_ABSTRACT of 'a * modification_action list + | DO_REPLACE + +let modify_opers replfun absfun oper_alist = + let failure () = + anomalylabstrm "generic__modify_opers" + [< 'sTR"An oper which was never supposed to appear has just appeared" ; + 'sPC ; 'sTR"Either this is in system code, and you need to" ; 'sPC; + 'sTR"report this error," ; 'sPC ; + 'sTR"Or you are using a user-written tactic which calls" ; 'sPC ; + 'sTR"generic__modify_opers, in which case the user-written code" ; + 'sPC ; 'sTR"is broken - this function is an internal system" ; + 'sPC ; 'sTR"for internal system use only" >] + in + let rec substrec = function + | DOPN(oper,cl) as c -> + let cl' = Array.map substrec cl in + (try + (match List.assoc oper oper_alist with + | NOT_OCCUR -> failure () + | DO_ABSTRACT (oper',modif) -> + if List.length modif > Array.length cl then + anomaly "found a reference with too few args" + else + interp_modif absfun oper (oper',modif) (Array.to_list cl') + | DO_REPLACE -> substrec (replfun (DOPN(oper,cl')))) + with + | Not_found -> DOPN(oper,cl')) + | DOP1(i,c) -> DOP1(i,substrec c) + | DOPL(oper,cl) -> DOPL(oper,List.map substrec cl) + | DOP2(oper,c1,c2) -> DOP2(oper,substrec c1,substrec c2) + | DLAM(na,c) -> DLAM(na,substrec c) + | DLAMV(na,v) -> DLAMV(na,Array.map substrec v) + | x -> x + in + if oper_alist = [] then fun x -> x else substrec + +let put_DLAMSV lna lc = + match lna with + | [] -> anomaly "put_DLAM" + | na::lrest -> List.fold_left (fun c na -> DLAM(na,c)) (DLAMV(na,lc)) lrest + +let put_DLAMSV_subst lid lc = + match lid with + | [] -> anomaly "put_DLAM" + | id::lrest -> + List.fold_left (fun c id' -> DLAM(Name id',subst_var id' c)) + (DLAMV(Name id,Array.map (subst_var id) lc)) lrest + +let rec decomp_DLAMV n = function + | DLAM(_,lc) -> decomp_DLAMV (n-1) lc + | DLAMV(_,lc) -> if n = 1 then lc else error "decomp_DLAMV 0" + | _ -> error "decomp_DLAMV 1" + +let decomp_DLAMV_name n = + let rec decomprec lna n = function + | DLAM(na,lc) -> decomprec (na::lna) (pred n) lc + | DLAMV(na,lc) -> if n = 1 then (na::lna,lc) else error "decomp_DLAMV 0" + | _ -> error "decomp_DLAMV 1" + in + decomprec [] n + +let decomp_all_DLAMV_name constr = + let rec decomprec lna = function + | DLAM(na,lc) -> decomprec (na::lna) lc + | DLAMV(na,lc) -> (na::lna,lc) + | _ -> assert false + in + decomprec [] constr + + +(* [Rel (n+m);...;Rel(n+1)] *) + +let rel_vect n m = Array.init m (fun i -> Rel(n+m-i)) + +let rel_list n m = + let rec reln l p = + if p>m then l else reln (Rel(n+p)::l) (p+1) + in + reln [] 1 + + +(* Hash-consing *) +let comp_term t1 t2 = + match (t1,t2) with + | (DOP0 o1, DOP0 o2) -> o1==o2 + | (DOP1(o1,t1), DOP1(o2,t2)) -> o1==o2 & t1==t2 + | (DOP2(o1,t1,u1), DOP2(o2,t2,u2)) -> o1==o2 & t1==t2 & u1==u2 + | (DOPN(o1,v1), DOPN(o2,v2)) -> + (o1==o2) & (Array.length v1 = Array.length v2) + & array_for_all2 (==) v1 v2 + | (DOPL(o1,l1), DOPL(o2,l2)) -> + (o1==o2) & (List.length l1 = List.length l2) + & List.for_all2 (==) l1 l2 + | (DLAM(x1,t1), DLAM(x2,t2)) -> x1==x2 & t1==t2 + | (DLAMV(x1,v1), DLAMV(x2,v2)) -> + (x1==x2) & (Array.length v1 = Array.length v2) + & array_for_all2 (==) v1 v2 + | (Rel i, Rel j) -> i=j + | (VAR x, VAR y) -> x==y + | _ -> false + +let hash_term (sh_rec,(sh_op,sh_na,sh_id)) t = + match t with + | DOP0 o -> DOP0 (sh_op o) + | DOP1(o,t) -> DOP1(sh_op o, sh_rec t) + | DOP2(o,t1,t2) -> DOP2(sh_op o, sh_rec t1, sh_rec t2) + | DOPN(o,v) -> DOPN(sh_op o, Array.map sh_rec v) + | DOPL(o,l) -> DOPL(sh_op o, List.map sh_rec l) + | DLAM(n,t) -> DLAM(sh_na n, sh_rec t) + | DLAMV(n,v) -> DLAMV(sh_na n, Array.map sh_rec v) + | Rel i -> t + | VAR x -> VAR (sh_id x) diff --git a/kernel/generic.mli b/kernel/generic.mli new file mode 100644 index 0000000000..c9d3dd73df --- /dev/null +++ b/kernel/generic.mli @@ -0,0 +1,116 @@ + +(* $Id$ *) + +open Util +open Names + +exception FreeVar +exception Occur + +type 'oper term = + | DOP0 of 'oper (* atomic terms *) + | DOP1 of 'oper * 'oper term (* operator of arity 1 *) + | DOP2 of 'oper * 'oper term * 'oper term (* operator of arity 2 *) + | DOPN of 'oper * 'oper term array (* operator of variadic arity *) + | DOPL of 'oper * 'oper term list (* operator of variadic arity *) + | DLAM of name * 'oper term (* deBruijn binder on one term*) + | DLAMV of name * 'oper term array (* deBruijn binder on many terms*) + | VAR of identifier (* named variable *) + | Rel of int (* variable as deBruijn index *) + +val isRel : 'a term -> bool +val isVAR : 'a term -> bool +val free_rels : 'a term -> Intset.t +val closedn : int -> 'a term -> unit +val closed0 : 'a term -> bool +val noccurn : int -> 'a term -> bool +val noccur_bet : int -> int -> 'a term -> bool + + +(* lifts *) +type lift_spec = + | ELID + | ELSHFT of lift_spec * int (* ELSHFT(l,n) == lift of n, then apply lift l *) + | ELLFT of int * lift_spec (* ELLFT(n,l) == apply l to de Bruijn > n *) + (* i.e under n binders *) +val el_shft : int -> lift_spec -> lift_spec +val el_lift : lift_spec -> lift_spec +val el_liftn : int -> lift_spec -> lift_spec +val reloc_rel: int -> lift_spec -> int + +(* explicit substitutions of type 'a *) +type 'a subs = + | ESID (* ESID = identity *) + | CONS of 'a * 'a subs (* CONS(t,S) = (S.t) parallel substitution *) + | SHIFT of int * 'a subs (* SHIFT(n,S) = (^n o S) terms in S are relocated *) + (* with n vars *) + | LIFT of int * 'a subs (* LIFT(n,S) = (%n S) stands for ((^n o S).n...1) *) + +val subs_cons : 'a * 'a subs -> 'a subs +val subs_lift : 'a subs -> 'a subs +val subs_shft : int * 'a subs -> 'a subs +val exp_rel : int -> int -> 'a subs -> (int * 'a, int) union +val expand_rel : int -> 'a subs -> (int * 'a, int) union + +type info = Closed | Open | Unknown +type 'a substituend = { mutable sinfo : info; sit : 'a } + +val exliftn : lift_spec -> 'a term -> 'a term +val liftn : int -> int -> 'a term -> 'a term +val lift : int -> 'a term -> 'a term +val pop : 'a term -> 'a term +val lift_substituend : int -> 'a term substituend -> 'a term +val make_substituend : 'a term -> 'a term substituend +val substn_many : 'a term substituend array -> int -> 'a term -> 'a term +val substl : 'a term list -> 'a term -> 'a term +val subst1 : 'a term -> 'a term -> 'a term +val occur_opern : 'a -> 'a term -> bool +val occur_oper0 : 'a -> 'a term -> bool +val occur_var : identifier -> 'a term -> bool +val occur_oper : 'a -> 'a term -> bool +val dependent : 'a term -> 'a term -> bool +val global_varsl : identifier list -> 'a term -> identifier list +val global_vars : 'a term -> identifier list +val global_vars_set : 'a term -> Idset.t +val subst_var : identifier -> 'a term -> 'a term +val subst_varn : identifier -> int -> 'a term -> 'a term +val replace_vars : + (identifier * 'a term substituend) list -> 'a term -> 'a term + +val rename_diff_occ : + identifier -> identifier list ->'a term -> identifier list * 'a term + +val sAPP : 'a term -> 'a term -> 'a term +val sAPPV : 'a term -> 'a term -> 'a term array +val sAPPVi : int -> 'a term -> 'a term -> 'a term + +val sAPPList : 'a term -> 'a term list -> 'a term +val sAPPVList : 'a term -> 'a term list-> 'a term array +val sAPPViList : int -> 'a term -> 'a term list -> 'a term +val under_dlams : ('a term -> 'a term) -> 'a term -> 'a term +val eq_term : 'a term -> 'a term -> bool + +type modification_action = ABSTRACT | ERASE + +type 'a modification = + | NOT_OCCUR + | DO_ABSTRACT of 'a * modification_action list + | DO_REPLACE + +val modify_opers : ('a term -> 'a term) -> ('a term -> 'a term -> 'a term) + -> ('a * 'a modification) list -> 'a term -> 'a term + +val put_DLAMSV : name list -> 'a term array -> 'a term +val decomp_DLAMV : int -> 'a term -> 'a term array +val decomp_DLAMV_name : int -> 'a term -> name list * 'a term array +val decomp_all_DLAMV_name : 'a term -> name list * 'a term array +val put_DLAMSV_subst : identifier list -> 'a term array -> 'a term +val rel_vect : int -> int -> 'a term array +val rel_list : int -> int -> 'a term list + +(* For hash-consing use *) +val hash_term : + ('a term -> 'a term) + * (('a -> 'a) * (name -> name) * (identifier -> identifier)) + -> 'a term -> 'a term +val comp_term : 'a term -> 'a term -> bool diff --git a/kernel/names.ml b/kernel/names.ml index af7f1f7195..e9de197fea 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -65,6 +65,14 @@ let id_ord id1 id2 = let id_without_number id = id.index = (-1) +module IdOrdered = + struct + type t = identifier + let compare = id_ord + end + +module Idset = Set.Make(IdOrdered) + (* Fresh names *) @@ -105,6 +113,9 @@ let get_new_ids n id lids = in get_rec n [] +let id_of_name default = function + | Name s -> s + | Anonymous -> default (* Kinds *) @@ -199,6 +210,8 @@ module SpOrdered = module Spset = Set.Make(SpOrdered) +module Spmap = Map.Make(SpOrdered) + (* Hash-consing of name objects *) module Hident = Hashcons.Make( struct diff --git a/kernel/names.mli b/kernel/names.mli index 5445065f7a..5d8791ba97 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -18,6 +18,7 @@ val index_of_id : identifier -> int val id_ord : identifier -> identifier -> int val id_without_number : identifier -> bool +module Idset : Set.S with type elt = identifier val lift_ident : identifier -> identifier val next_ident_away_from : identifier -> identifier list -> identifier @@ -27,6 +28,7 @@ val next_name_away_with_default : string -> name -> identifier list -> identifier val get_new_ids : int -> identifier -> identifier list -> identifier list +val id_of_name : identifier -> name -> identifier type path_kind = CCI | FW | OBJ @@ -58,6 +60,7 @@ val sp_ord : section_path -> section_path -> int val sp_gt : section_path * section_path -> bool module Spset : Set.S with type elt = section_path +module Spmap : Map.S with type key = section_path (* Hash-consing *) val hcons_names : unit -> diff --git a/kernel/sign.ml b/kernel/sign.ml index 7aa3f75e9a..35731c7341 100644 --- a/kernel/sign.ml +++ b/kernel/sign.ml @@ -3,6 +3,8 @@ open Names open Util +open Generic +open Term (* Signatures *) @@ -139,6 +141,28 @@ let prepend_sign gamma1 gamma2 = else invalid_arg "prepend_sign" +let dunbind default sign ty = function + | DLAM(na,c) -> + let id = next_ident_away (id_of_name default na) (ids_of_sign sign) in + (add_sign (id,ty) sign, subst1 (VAR id) c) + | _ -> invalid_arg "dunbind default" + +let dunbindv default sign ty = function + | DLAMV(na,c) -> + let id = next_ident_away (id_of_name default na) (ids_of_sign sign) in + (add_sign (id,ty) sign,Array.map (subst1 (VAR id)) c) + | _ -> invalid_arg "dunbindv default" + +let dbind sign c = + let (id,ty) = hd_sign sign + and sign' = tl_sign sign in + (ty,DLAM(Name id,subst_var id c)) + +let dbindv sign cl = + let (id,ty) = hd_sign sign + and sign' = tl_sign sign in + (ty,DLAMV(Name id,Array.map (subst_var id) cl)) + (* Signatures + de Bruijn environments *) @@ -207,3 +231,7 @@ let lookup_id id env = with | Not_found -> let (x,y) = lookup_glob id env in GLOBNAME(x,y) + +type 'b assumptions = (type_judgment,'b) env +type environment = (type_judgment,type_judgment) env +type context = type_judgment signature diff --git a/kernel/sign.mli b/kernel/sign.mli index 2cbab3672d..b07fcd0310 100644 --- a/kernel/sign.mli +++ b/kernel/sign.mli @@ -2,6 +2,8 @@ (* $Id$ *) open Names +open Generic +open Term type 'a signature = identifier list * 'a list type 'a db_signature = (name * 'a) list @@ -40,6 +42,13 @@ val add_sign_replacing : identifier -> (identifier * 'a) -> 'a signature -> 'a signature val prepend_sign : 'a signature -> 'a signature -> 'a signature +val dunbind : identifier -> 'a signature -> 'a -> 'b term + -> 'a signature * 'b term +val dunbindv : identifier -> 'a signature -> 'a -> 'b term + -> 'a signature * 'b term array +val dbind : 'a signature -> 'b term -> 'a * 'b term +val dbindv : 'a signature -> 'b term array -> 'a * 'b term + val gLOB : 'b signature -> ('b,'a) env @@ -66,3 +75,6 @@ type ('b,'a) search_result = val lookup_id : identifier -> ('b,'a) env -> ('b,'a) search_result +type 'b assumptions = (type_judgment,'b) env +type environment = (type_judgment,type_judgment) env +type context = type_judgment signature diff --git a/kernel/term.ml b/kernel/term.ml new file mode 100644 index 0000000000..0e8a8cdaaf --- /dev/null +++ b/kernel/term.ml @@ -0,0 +1,1489 @@ + +(* $Id$ *) + +(* This module instanciates the structure of generic deBruijn terms to Coq *) + +open Util +open Pp +open Names +open Generic +open Univ + +(* Coq abstract syntax with deBruijn variables; 'a is the type of sorts *) + +type 'a oper = + (* DOP0 *) + | Meta of int + | Sort of 'a + | Implicit + (* DOP2 *) + | Cast | Prod | Lambda + (* DOPN *) + | AppL | Const of section_path | Abst of section_path + | MutInd of section_path * int + | MutConstruct of (section_path * int) * int + | MutCase of case_info + | Fix of int array * int + | CoFix of int + + | XTRA of string * Coqast.t list + (* an extra slot, for putting in whatever sort of + operator we need for whatever sort of application *) + +and case_info = (section_path * int) option + +(* Sorts. *) + +type contents = Pos | Null + +let contents_of_str = function + | "Pos" -> Pos + | "Null" -> Null + | _ -> invalid_arg "contents_of_str" + +let str_of_contents = function + | Pos -> "Pos" + | Null -> "Null" + +type sorts = + | Prop of contents (* proposition types *) + | Type of universe + +let mk_Set = Prop Pos +let mk_Prop = Prop Null + +type constr = sorts oper term + +type 'a judge = { body : constr; typ : 'a } + +type type_judgment = sorts judge +type term_judgment = type_judgment judge + +type conv_pb = CONV | CONV_LEQ | CONV_X | CONV_X_LEQ + +(****************************************************************************) +(* Functions for dealing with constr terms *) +(****************************************************************************) + +(*********************) +(* Term constructors *) +(*********************) + +(* Constructs a DeBrujin index with number n *) +let mkRel n = (Rel n) + +(* Constructs an existential variable named "?" *) +let mkExistential = (DOP0 (XTRA ("ISEVAR",[]))) + +(* Constructs an existential variable named "?n" *) +let mkMeta n = DOP0 (Meta n) + +(* Constructs a Variable named id *) +let mkVar id = VAR id + +(* Construct an XTRA term (XTRA is an extra slot for whatever you want) *) +let mkXtra s astlist = (DOP0 (XTRA (s, astlist))) + +(* Construct a type *) +let mkSort s = DOP0 (Sort s) +let mkProp = DOP0 (Sort mk_Prop) +let mkSet = DOP0 (Sort mk_Set) +let mkType u = DOP0 (Sort (Type u)) + +let prop = Prop Null +and spec = Prop Pos +and types = Type dummy_univ +and type_0 = Type prop_univ +and type_1 = Type prop_univ_univ + +(* Construct an implicit (see implicit arguments in the RefMan) *) +(* let mkImplicit = DOP0 Implicit*) + +let implicit_univ = make_path ["Implicit"] (id_of_string "dummy") OBJ +let implicit_sort = Type { u_sp = implicit_univ ; u_num = 0} +let mkImplicit = DOP0 (Sort implicit_sort) + + +(* 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 = + match t1 with + | DOP2(Cast,t,_) -> DOP2(Cast,t,t2) + | _ -> (DOP2 (Cast,t1,t2)) + +(* Constructs the product (x:t1)t2 *) +let mkProd x t1 t2 = (DOP2 (Prod,t1,(DLAM (x,t2)))) + +(* non-dependant product t1 -> t2 *) +let mkArrow t1 t2 = mkProd Anonymous t1 t2 + +(* named product *) +let mkNamedProd name typ c = mkProd (Name name) typ (subst_var name c) + +(* Constructs the abstraction [x:t1]t2 *) +let mkLambda x t1 t2 = (DOP2 (Lambda,t1,(DLAM (x,t2)))) +let mkNamedLambda name typ c = mkLambda (Name name) typ (subst_var name c) + +(* If lt = [t1; ...; tn], constructs the application (t1 ... tn) *) +let mkAppL a = DOPN (AppL, a) +let mkAppList l = DOPN (AppL, Array.of_list l) + +(* Constructs a constant *) +(* The array of terms correspond to the variables introduced in the section *) +let mkConst sp a = DOPN (Const sp, a) + +(* Constructs an abstract object *) +let mkAbst sp a = DOPN (Abst sp, a) + +(* Constructs the ith (co)inductive type of the block named sp *) +(* The array of terms correspond to the variables introduced in the section *) +let mkMutInd sp i l = (DOPN (MutInd (sp,i), l)) + +(* Constructs the jth constructor of the ith (co)inductive type of the + block named sp. The array of terms correspond to the variables + introduced in the section *) +let mkMutConstruct sp i j l = (DOPN ((MutConstruct ((sp,i),j),l))) + +(* Constructs the term <p>Case c of c1 | c2 .. | cn end *) +let mkMutCase ci p c ac = DOPN (MutCase ci,Array.append [|p;c|] (Array.of_list ac)) +let mkMutCaseA ci p c ac = DOPN (MutCase ci,Array.append [|p;c|] ac) + +(* If recindxs = [|i1,...in|] + typarray = [|t1,...tn|] + funnames = [f1,.....fn] + bodies = [b1,.....bn] + then + + mkFix recindxs i typarray funnames bodies + + constructs the ith function of the block + + Fixpoint f1 [ctx1] = b1 + with f2 [ctx2] = b2 + ... + with fn [ctxn] = bn. + + where the lenght of the jth context is ij. + + Warning: as an invariant the ti are casted during the Fix formation; + these casts are then used by destFix +*) +let in_fixcast {body=b; typ=s} = DOP2 (Cast, b, DOP0 (Sort s)) + +(* Here, we assume the body already constructed *) +let mkFixDlam recindxs i jtypsarray body = + let typsarray = Array.map in_fixcast jtypsarray in + DOPN (Fix (recindxs,i),Array.append typsarray body) + +let mkFix recindxs i jtypsarray funnames bodies = + let rec wholebody l = + match l with + | [h] -> (DLAMV (h,bodies)) + | (x::l) -> (DLAM (x, wholebody l)) + | [] -> anomaly "in Term.mkFix : empty list of funnames" + in + mkFixDlam recindxs i jtypsarray [|(wholebody funnames)|] + +(* If typarray = [|t1,...tn|] + funnames = [f1,.....fn] + bodies = [b1,.....bn] + then + + mkCoFix i typsarray funnames bodies + + constructs the ith function of the block + + CoFixpoint f1 = b1 + with f2 = b2 + ... + with fn = bn. + +*) +(* Here, we assume the body already constructed *) +let mkCoFixDlam i jtypsarray body = + let typsarray = Array.map in_fixcast jtypsarray in + DOPN ((CoFix i),(Array.append typsarray body)) + +let mkCoFix i jtypsarray funnames bodies = + let rec wholebody l = + match l with + | [h] -> (DLAMV (h,bodies)) + | (x::l) -> (DLAM (x, wholebody l)) + | [] -> anomaly "in Term.mkCoFix : empty list of funnames" + in + mkCoFixDlam i jtypsarray [|(wholebody funnames)|] + +(********************) +(* Term destructors *) +(********************) + +(* Destructor operations : partial functions + Raise invalid_arg "dest*" if the const has not the expected form *) + +(* Destructs a DeBrujin index *) +let destRel = function + | (Rel n) -> n + | _ -> invalid_arg "destRel" + +(* Destructs an existential variable *) +let destMeta = function + | (DOP0 (Meta n)) -> n + | _ -> invalid_arg "destMeta" + +let isMETA = function DOP0(Meta _) -> true | _ -> false + +(* Destructs a variable *) +let destVar = function + | (VAR id) -> id + | _ -> invalid_arg "destVar" + +(* Destructs an XTRA *) +let destXtra = function + | DOP0 (XTRA (s,astlist)) -> (s,astlist) + | _ -> invalid_arg "destXtra" + +(* Destructs a type *) +let destSort = function + | (DOP0 (Sort s)) -> s + | _ -> invalid_arg "destSort" + +let rec isprop = function + | DOP0(Sort(Prop _)) -> true + | DOP2(Cast,c,_) -> isprop c + | _ -> false + +let rec is_Prop = function + | DOP0(Sort(Prop Null)) -> true + | DOP2(Cast,c,_) -> is_Prop c + | _ -> false + +let rec is_Set = function + | DOP0(Sort(Prop Pos)) -> true + | DOP2(Cast,c,_) -> is_Set c + | _ -> false + +let rec is_Type = function + | DOP0(Sort(Type _)) -> true + | DOP2(Cast,c,_) -> is_Type c + | _ -> false + +let isType = function + | Type _ -> true + | _ -> false + +let is_small = function + | Prop _ -> true + | _ -> false + +let iskind c = isprop c or is_Type c + +let same_kind c1 c2 = (isprop c1 & isprop c2) or (is_Type c1 & is_Type c2) + +let rec contents_of_kind = function + | DOP0(Sort(Prop cts)) -> cts + | DOP0(Sort(Type _)) -> Pos + | DOP2(Cast,c,t) -> contents_of_kind c + | _ -> invalid_arg "contents_of_kind" + +(* Destructs a casted term *) +let destCast = function + | DOP2 (Cast, t1, t2) -> (t1,t2) + | _ -> invalid_arg "destCast" + +let isCast = function DOP2(Cast,_,_) -> true | _ -> false + +let cast_term = function + | DOP2(Cast,c,t) -> c + | _ -> anomaly "found a type which did not contain a cast (cast_term)" + +let cast_type = function + | DOP2(Cast,c,t) -> t + | _ -> anomaly "found a type which did not contain a cast (cast_type)" + +let rec strip_outer_cast = function + | DOP2(Cast,c,_) -> strip_outer_cast c + | c -> c + +(* Destructs the product (x:t1)t2 *) +let destProd = function + | DOP2 (Prod, t1, (DLAM (x,t2))) -> (x,t1,t2) + | _ -> invalid_arg "destProd" + +let rec hd_of_prod prod = + match strip_outer_cast prod with + | DOP2(Prod,c,DLAM(n,t')) -> hd_of_prod t' + | t -> t + +let hd_is_constructor t = + let is_constructor = function + | DOPN(MutConstruct((sp,tyi),i),cl)-> true + | _ ->false + in + match t with + | DOPN(AppL,v) -> is_constructor v.(0) + | c -> is_constructor c + +(* Destructs the abstraction [x:t1]t2 *) +let destLambda = function + | DOP2 (Lambda, t1, (DLAM (x,t2))) -> (x,t1,t2) + | _ -> invalid_arg "destLambda" + +(* Destructs an application *) +let destAppL = function + | (DOPN (AppL,a)) -> a + | _ -> invalid_arg "destAppL" + +let isAppL = function DOPN(AppL,_) -> true | _ -> false + +let args_app = function + | DOPN(AppL,cl) -> if Array.length cl >1 then array_tl cl else [||] + | c -> [||] + +let hd_app = function + | DOPN(AppL,cl) -> cl.(0) + | c -> c + +(* Destructs a constant *) +let destConst = function + | DOPN (Const sp, a) -> (sp, a) + | _ -> invalid_arg "destConst" + +let path_of_const = function + | DOPN (Const sp,_) -> sp + | _ -> anomaly "path_of_const called with bad args" + +let args_of_const = function + | DOPN (Const _,args) -> args + | _ -> anomaly "args_of_const called with bad args" + +(* Destructs an abstract term *) +let destAbst = function + | DOPN (Abst sp, a) -> (sp, a) + | _ -> invalid_arg "destAbst" + +let path_of_abst = function + | DOPN(Abst sp,_) -> sp + | _ -> anomaly "path_of_abst called with bad args" + +let args_of_abst = function + | DOPN(Abst _,args) -> args + | _ -> anomaly "args_of_abst called with bad args" + +(* Destructs a (co)inductive type named sp *) +let destMutInd = function + | DOPN (MutInd (sp,i), l) -> (sp,i,l) + | _ -> invalid_arg "destMutInd" + +let op_of_mind = function + | DOPN(MutInd (sp,i),_) -> (sp,i) + | _ -> anomaly "op_of_mind called with bad args" + +let args_of_mind = function + | DOPN(MutInd _,args) -> args + | _ -> anomaly "args_of_mind called with bad args" + +let ci_of_mind = function + | DOPN(MutInd(sp,tyi),_) -> Some (sp,tyi) + | _ -> invalid_arg "ci_of_mind" + +(* Destructs a constructor *) +let destMutConstruct = function + | DOPN (MutConstruct ((sp,i),j),l) -> (sp,i,j,l) + | _ -> invalid_arg "dest" + +let op_of_mconstr = function + | DOPN(MutConstruct (spi,c),_) -> (spi,c) + | _ -> anomaly "op_of_mconstr called with bad args" + +let args_of_mconstr = function + | DOPN(MutConstruct _,args) -> args + | _ -> anomaly "args_of_mconstr called with bad args" + +(* Destructs a term <p>Case c of lc1 | lc2 .. | lcn end *) +let destCase = function + | DOPN (MutCase ci,v) -> (ci,v.(0),v.(1),Array.sub v 2 (Array.length v - 2)) + | _ -> anomaly "destCase" + +(* Destructs the ith function of the block + Fixpoint f1 [ctx1] = b1 + with f2 [ctx2] = b2 + ... + with fn [ctxn] = bn. + + where the lenght of the jth context is ij. +*) + +let out_fixcast = function + | DOP2 (Cast, b, DOP0 (Sort s)) -> { body = b; typ = s } + | _ -> anomaly "destFix: malformed recursive definition" + +let destGralFix a = + let nbofdefs = Array.length a in + let types = Array.sub a 0 (nbofdefs-1) in + let dlambody = a.(nbofdefs-1) in + let rec destbody l c = + match c with + | DLAMV (h,bodies) -> (List.rev (h::l), bodies) + | DLAM (x,t) -> destbody (x::l) t + | _ -> invalid_arg "destGralFix" + in + let funnames,bodies = destbody [] dlambody in + (types,funnames,bodies) + +let destFix = function + | DOPN (Fix (recindxs,i),a) -> + let (types,funnames,bodies) = destGralFix a in + (recindxs,i,Array.map out_fixcast types,funnames,bodies) + | _ -> invalid_arg "destFix" + +let destCoFix = function + | DOPN ((CoFix i),a) -> + let (types,funnames,bodies) = destGralFix a in + (i,Array.map out_fixcast types,funnames,bodies) + | _ -> invalid_arg "destCoFix" + +(* Provisoire, le temps de maitriser les cast *) +let destUntypedFix = function + | DOPN (Fix (recindxs,i),a) -> + let (types,funnames,bodies) = destGralFix a in + (recindxs,i,types,funnames,bodies) + | _ -> invalid_arg "destFix" + +let destUntypedCoFix = function + | DOPN (CoFix i,a) -> + let (types,funnames,bodies) = destGralFix a in + (i,types,funnames,bodies) + | _ -> invalid_arg "destCoFix" + + +(******************) +(* Term analysis *) +(******************) + +type kindOfTerm = + | IsRel of int + | IsMeta of int + | IsVar of identifier + | IsXtra of string * (Coqast.t list) + | IsSort of sorts + | IsImplicit + | IsCast of constr*constr + | IsProd of name*constr*constr + | IsLambda of name*constr*constr + | IsAppL of constr array + | IsConst of section_path*constr array + | IsAbst of section_path*constr array + | IsMutInd of section_path*int*constr array + | IsMutConstruct of section_path*int*int*constr array + | IsMutCase of case_info*constr*constr*(constr array) + | IsFix of (int array)*int* + (constr array)*(name list)*(constr array) + | IsCoFix of int*(constr array) * + (name list)*(constr array) + + +(* Discriminates which kind of term is it. + + Note that there is no cases for DLAM and DLAMV. These terms do not + make sense alone, but they must be preceeded by the application of + an operator. *) + +let kind_of_term c = + match c with + | Rel n -> IsRel n + | VAR id -> IsVar id + | DOP0 (Meta n) -> IsMeta n + | DOP0 (Sort s) -> IsSort s + | DOP0 (XTRA (s, astlist)) -> IsXtra (s,astlist) + | DOP0 Implicit -> IsImplicit + | DOP2 (Cast, t1, t2) -> IsCast (t1,t2) + | DOP2 (Prod, t1, (DLAM (x,t2))) -> IsProd (x,t1,t2) + | DOP2 (Lambda, t1, (DLAM (x,t2))) -> IsLambda (x,t1,t2) + | DOPN (AppL,a) -> IsAppL a + | DOPN (Const sp, a) -> IsConst (sp,a) + | DOPN (Abst sp, a) -> IsAbst (sp, a) + | DOPN (MutInd (sp,i), l) -> IsMutInd (sp,i,l) + | DOPN (MutConstruct ((sp,i), j),l) -> IsMutConstruct (sp,i,j,l) + | DOPN (MutCase ci,v) -> + IsMutCase (ci,v.(0),v.(1),Array.sub v 2 (Array.length v - 2)) + | DOPN ((Fix (recindxs,i),a)) -> + let (types,funnames,bodies) = destGralFix a in + IsFix (recindxs,i,types,funnames,bodies) + | DOPN ((CoFix i),a) -> + let (types,funnames,bodies) = destGralFix a in + IsCoFix (i,types,funnames,bodies) + | _ -> errorlabstrm "Term.kind_of_term" [< 'sTR "ill-formed constr" >] + +(***************************) +(* Other term constructors *) +(***************************) + +let abs_implicit c = mkLambda Anonymous mkImplicit c +let lambda_implicit a = mkLambda (Name(id_of_string"y")) mkImplicit a +let lambda_implicit_lift n a = iterate lambda_implicit n (lift n a) + +(* prod_it b [x1:T1;..xn:Tn] = (x1:T1)..(xn:Tn)b *) +let prod_it = List.fold_left (fun c (n,t) -> mkProd n t c) + +(* lam_it b [x1:T1;..xn:Tn] = [x1:T1]..[xn:Tn]b *) +let lam_it = List.fold_left (fun c (n,t) -> mkLambda n t c) + +(* prodn n ([x1:T1]..[xn:Tn]Gamma) b = (x1:T1)..(xn:Tn)b *) +let prodn n env b = + let rec prodrec = function + | (0, env, b) -> b + | (n, ((v,t)::l), b) -> prodrec (n-1, l, DOP2(Prod,t,DLAM(v,b))) + | _ -> assert false + in + prodrec (n,env,b) + +(* lamn n ([x1:T1]..[xn:T]Gamma) b = [x1:T1]..[xn:Tn]b *) +let lamn n env b = + let rec lamrec = function + | (0, env, b) -> b + | (n, ((v,t)::l), b) -> lamrec (n-1, l, DOP2(Lambda,t,DLAM(v,b))) + | _ -> assert false + in + lamrec (n,env,b) + +let rec applist = function + | (f,[]) -> f + | (DOPN(AppL,cl),l2) -> + let c = array_hd cl in + if isAppL c then + applist(c,array_app_tl cl l2) + else + DOPN(AppL,Array.append cl (Array.of_list l2)) + | (f,l) -> DOPN(AppL,Array.of_list(f::l)) + +and applistc f l = applist(f,l) + +let rec appvect = function + | (f, [||]) -> f + | (DOPN(AppL,cl), v) -> + let c = array_hd cl in + if isAppL c then + appvect (c, Array.append (array_tl cl) v) + else + DOPN(AppL, Array.append cl v) + | (f,v) -> DOPN(AppL, array_cons f v) + +and appvectc f l = appvect (f,l) + +(* to_lambda n (x1:T1)...(xn:Tn)(xn+1:Tn+1)...(xn+j:Tn+j)T = + * [x1:T1]...[xn:Tn](xn+1:Tn+1)...(xn+j:Tn+j)T *) +let rec to_lambda n prod = + if n=0 then + prod + else + match prod with + | DOP2(Prod,ty,DLAM(na,bd)) -> + DOP2(Lambda,ty,DLAM(na, to_lambda (n-1) bd)) + | DOP2(Cast,c,_) -> to_lambda n c + | _ -> errorlabstrm "to_lambda" [<>] + +let rec to_prod n lam = + if n=0 then + lam + else + match lam with + | DOP2(Lambda,ty,DLAM(na,bd)) -> + DOP2(Prod,ty,DLAM(na, to_prod (n-1) bd)) + | DOP2(Cast,c,_) -> to_prod n c + | _ -> errorlabstrm "to_prod" [<>] + +(* pseudo-reduction rule: + * [prod_app s (Prod(_,B)) N --> B[N] + * with an strip_outer_cast on the first argument to produce a product. + * if this does not work, then we use the string S as part of our + * error message. + *) + +let prod_app s t n = + match strip_outer_cast t with + | DOP2(Prod,_,b) -> sAPP b n + | _ -> + errorlabstrm s [< 'sTR"Needed a product, but didn't find one in " ; + 'sTR s ; 'fNL >] + + +(* prod_appvect s T [| a1 ; ... ; an |] -> (T a1 ... an) *) +let prod_appvect s t nL = Array.fold_left (prod_app s) t nL + +(* prod_applist s T [ a1 ; ... ; an ] -> (T a1 ... an) *) +let prod_applist s t nL = List.fold_left (prod_app s) t nL + + +(*********************************) +(* Other term destructors *) +(*********************************) + +(* Transforms a product term (x1:T1)..(xn:Tn)T into the pair + ([(xn,Tn);...;(x1,T1)],T), where T is not a product *) +let decompose_prod = + let rec prodec_rec l = function + | DOP2(Prod,t,DLAM(x,c)) -> prodec_rec ((x,t)::l) c + | DOP2(Cast,c,_) -> prodec_rec l c + | c -> l,c + in + prodec_rec [] + +(* Transforms a lambda term [x1:T1]..[xn:Tn]T into the pair + ([(xn,Tn);...;(x1,T1)],T), where T is not a lambda *) +let decompose_lam = + let rec lamdec_rec l = function + | DOP2(Lambda,t,DLAM(x,c)) -> lamdec_rec ((x,t)::l) c + | DOP2(Cast,c,_) -> lamdec_rec l c + | c -> l,c + in + lamdec_rec [] + +(* Given a positive integer n, transforms a product term (x1:T1)..(xn:Tn)T + into the pair ([(xn,Tn);...;(x1,T1)],T) *) +let decompose_prod_n n = + if n < 0 then + error "decompose_prod_n: integer parameter must be positive" + else + let rec prodec_rec l n c = + if n=0 then l,c + else match c with + | DOP2(Prod,t,DLAM(x,c)) -> prodec_rec ((x,t)::l) (n-1) c + | DOP2(Cast,c,_) -> prodec_rec l n c + | c -> error "decompose_prod_n: not enough products" + in + prodec_rec [] n + +(* Given a positive integer n, transforms a lambda term [x1:T1]..[xn:Tn]T + into the pair ([(xn,Tn);...;(x1,T1)],T) *) +let decompose_lam_n n = + if n < 0 then + error "decompose_lam_n: integer parameter must be positive" + else + let rec lamdec_rec l n c = + if n=0 then l,c + else match c with + | DOP2(Lambda,t,DLAM(x,c)) -> lamdec_rec ((x,t)::l) (n-1) c + | DOP2(Cast,c,_) -> lamdec_rec l n c + | c -> error "decompose_lam_n: not enough abstractions" + in + lamdec_rec [] n + +(* (nb_lam [na1:T1]...[nan:Tan]c) where c is not an abstraction + * gives n (casts are ignored) *) +let nb_lam = + let rec nbrec n = function + | DOP2(Lambda,_,DLAM(_,c)) -> nbrec (n+1) c + | DOP2(Cast,c,_) -> nbrec n c + | _ -> n + in + nbrec 0 + +(* similar to nb_lam, but gives the number of products instead *) +let nb_prod = + let rec nbrec n = function + | DOP2(Prod,_,DLAM(_,c)) -> nbrec (n+1) c + | DOP2(Cast,c,_) -> nbrec n c + | _ -> n + in + nbrec 0 + +(********************************************************************) +(* various utility functions for implementing terms with bindings *) +(********************************************************************) + +let extract_lifted (n,x) = lift n x +let insert_lifted x = (0,x) + +(* l is a list of pairs (n:nat,x:constr), env is a stack of (na:name,T:constr) + push_and_lift adds a component to env and lifts l one step *) +let push_and_lift (na,t) env l = + ((na,t)::env, List.map (fun (n,x) -> (n+1,x)) l) + + +(* if T is not (x1:A1)(x2:A2)....(xn:An)T' then (push_and_liftl n env T l) + raises an error else it gives ([x1,A1 ; x2,A2 ; ... ; xn,An]@env,T',l') + where l' is l lifted n steps *) +let push_and_liftl n env t l = + let rec pushrec n t (env,l) = + match (n,t) with + | (0, _) -> (env,t,l) + | (_, DOP2(Prod,t,DLAM(na,b))) -> + pushrec (n-1) b (push_and_lift (na,t) env l) + | (_, DOP2(Cast,t,_)) -> pushrec n t (env,l) + | _ -> error "push_and_liftl" + in + pushrec n t (env,l) + +(* if T is not (x1:A1)(x2:A2)....(xn:An)T' then (push_and_liftl n env T l) + raises an error else it gives ([x1,A1 ; x2,A2 ; ... ; xn,An]@env,T',l') + where l' is l lifted n steps *) +let push_lam_and_liftl n env t l = + let rec pushrec n t (env,l) = + match (n,t) with + | (0, _) -> (env,t,l) + | (_, DOP2(Lambda,t,DLAM(na,b))) -> + pushrec (n-1) b (push_and_lift (na,t) env l) + | (_, DOP2(Cast,t,_)) -> pushrec n t (env,l) + | _ -> error "push_lam_and_liftl" + in + pushrec n t (env,l) + +(* l is a list of pairs (n:nat,x:constr), tlenv is a stack of +(na:name,T:constr), B : constr, na : name +(prod_and_pop ((na,T)::tlenv) B l) gives (tlenv, (na:T)B, l') +where l' is l lifted down one step *) +let prod_and_pop env b l = + match env with + | [] -> error "prod_and_pop" + | (na,t)::tlenv -> + (tlenv,DOP2(Prod,t,DLAM(na,b)), + List.map (function + (0,x) -> (0,lift (-1) x) + | (n,x) -> (n-1,x)) l) + +(* recusively applies prod_and_pop : +if env = [na1:T1 ; na2:T2 ; ... ; nan:Tn]@tlenv +then +(prod_and_popl n env T l) gives (tlenv,(nan:Tn)...(na1:Ta1)T,l') where +l' is l lifted down n steps *) +let prod_and_popl n env t l = + let rec poprec = function + | (0, (env,b,l)) -> (env,b,l) + | (n, ([],_,_)) -> error "prod_and_popl" + | (n, (env,b,l)) -> poprec (n-1, prod_and_pop env b l) + in + poprec (n,(env,t,l)) + +(* similar to prod_and_pop, but gives [na:T]B intead of (na:T)B *) +let lam_and_pop env b l = + match env with + | [] -> error "lam_and_pop" + | (na,t)::tlenv -> + (tlenv,DOP2(Lambda,t,DLAM(na,b)), + List.map (function + (0,x) -> (0,lift (-1) x) + | (n,x) -> (n-1,x)) l) + +(* similar to lamn_and_pop but generates new names whenever the name is + * Anonymous *) +let lam_and_pop_named env body l acc_ids = + match env with + | [] -> error "lam_and_pop" + | (na,t)::tlenv -> + let id = match na with + | Anonymous -> next_ident_away (id_of_string "a") acc_ids + | Name id -> id + in + (tlenv,DOP2(Lambda,t,DLAM((Name id),body)), + List.map (function + | (0,x) -> (0,lift (-1) x) + | (n,x) -> (n-1,x)) l, + (id::acc_ids)) + +(* similar to prod_and_popl but gives [nan:Tan]...[na1:Ta1]B instead of + * (nan:Tan)...(na1:Ta1)B *) +let lam_and_popl n env t l = + let rec poprec = function + | (0, (env,b,l)) -> (env,b,l) + | (n, ([],_,_)) -> error "lam_and_popl" + | (n, (env,b,l)) -> poprec (n-1, lam_and_pop env b l) + in + poprec (n,(env,t,l)) + +(* similar to prod_and_popl but gives [nan:Tan]...[na1:Ta1]B instead of + * but it generates names whenever nai=Anonymous *) + +let lam_and_popl_named n env t l = + let rec poprec = function + | (0, (env,b,l,_)) -> (env,b,l) + | (n, ([],_,_,_)) -> error "lam_and_popl" + | (n, (env,b,l,acc_ids)) -> poprec (n-1, lam_and_pop_named env b l acc_ids) + in + poprec (n,(env,t,l,[])) + +(* [lambda_ize n T endpt] + * will pop off the first n products in T, then stick in endpt, + * properly lifted, and then push back the products, but as lambda- + * abstractions *) +let lambda_ize n t endpt = + let env = [] + and carry = [insert_lifted endpt] in + let env, endpt = + match push_and_liftl n env t carry with + | (env,_,[endpt]) -> env, endpt + | _ -> anomaly "bud in Term.lamda_ize" + in + let t = extract_lifted endpt in + match lam_and_popl n env t [] with + | (_,t,[]) -> t + | _ -> anomaly "bud in Term.lamda_ize" + +let sort_hdchar = function + | Prop(_) -> "P" + | Type(_) -> "T" + +let pb_is_univ_adjust pb = + pb = CONV or pb = CONV_LEQ + +let pb_is_equal pb = + pb = CONV or pb = CONV_X + +let pb_equal = function + | CONV_LEQ -> CONV + | CONV_X_LEQ -> CONV_X + | pb -> pb + +(* Level comparison for information extraction : Prop <= Type *) +let le_kind l m = (isprop l) or (is_Type m) + +let le_kind_implicit k1 k2 = + (k1=mkImplicit) or (isprop k1) or (k2=mkImplicit) or (is_Type k2) + +(******************************************************************) +(* Flattening and unflattening of embedded applications and casts *) +(******************************************************************) + +(* N.B.: does NOT collapse AppLs ! *) +let ensure_appl = function + | DOPN(AppL,_) as t -> t + | t -> DOPN(AppL,[|t|]) + +(* unflattens application lists *) +let rec telescope_appl = function + | DOPN(AppL,cl) -> + array_fold_left_from 1 (fun c e -> DOPN(AppL,[|c;e|])) (array_hd cl) cl + | c -> c + +(* flattens application lists *) +let rec collapse_appl = function + | DOPN(AppL,cl) -> + let rec collapse_rec = function + | (DOPN(AppL,cl),l2) -> collapse_rec(array_hd cl,array_app_tl cl l2) + | (DOP2(Cast,DOPN(AppL,cl),t),l) -> collapse_rec(DOPN(AppL,cl),l) + | (f,[]) -> f + | (f,l) -> let v = Array.of_list (f::l) in DOPN(AppL,v) + in + collapse_rec (array_hd cl, array_list_of_tl cl) + | c -> c + +let rec decomp_app c = + match collapse_appl c with + | DOPN(AppL,cl) -> (array_hd cl, array_list_of_tl cl) + | DOP2(Cast,c,t) -> decomp_app c + | c -> (c,[]) + +(* strips head casts and flattens head applications *) +let strip_head_cast = function + | DOPN(AppL,cl) -> + let rec collapse_rec = function + | (DOPN(AppL,cl),l2) -> collapse_rec(array_hd cl, array_app_tl cl l2) + | (DOP2(Cast,c,t),l) -> collapse_rec(c,l) + | (f,[]) -> f + | (f,l) -> let v = Array.of_list (f::l) in DOPN(AppL,v) + in + collapse_rec(array_hd cl, array_app_tl cl []) + | c -> c + +(* (occur_const (s:section_path) c) -> true if constant s occurs in c, + * false otherwise *) +let occur_const s = occur_opern (Const s) + +(* let sigma be a finite function mapping sections paths to + constants represented as (identifier list * constr) option. + (replace_consts sigma M) unfold_one_id the constants from sigma in term M + + - if (sp,NONE) is in sigma then the constant should not appear in + term M otherwise replace_consts raises an anomaly ; + + - if (sp,SOME (idl,c)), then the constant sp is replaced by + c in which the variables given by idl are replaced by the arguments + of (Const sp), if the number of variables and arguments are not equal + an anomaly is raised ; + + - if no (sp,_) appears in sigma, then sp is not unfolded. + + NOTE : the case of DOPL is not handled... +*) +let replace_consts const_alist = + let rec substrec = function + | DOPN(Const sp,cl) as c -> + let cl' = Array.map substrec cl in + (try + match List.assoc sp const_alist with + | Some (hyps,body) -> + if List.length hyps <> Array.length cl then + anomaly "found a constant with a bad number of args" + else + replace_vars + (List.combine hyps + (array_map_to_list make_substituend cl')) body + | None -> anomaly ("a constant which was never"^ + " supposed to appear has just appeared") + with Not_found -> DOPN(Const sp,cl')) + + | DOP1(i,c) -> DOP1(i,substrec c) + | DOPN(oper,cl) -> DOPN(oper,Array.map substrec cl) + | DOP2(oper,c1,c2) -> DOP2(oper,substrec c1,substrec c2) + | DLAM(na,c) -> DLAM(na,substrec c) + | DLAMV(na,v) -> DLAMV(na,Array.map substrec v) + | x -> x + in + if const_alist = [] then function x -> x else substrec + +(* NOTE : the case of DOPL is not handled by whd_castapp_stack *) +let whd_castapp_stack = + let rec whrec x stack = match x with + | DOPN(AppL,cl) -> whrec (array_hd cl) (array_app_tl cl stack) + | DOP2(Cast,c,_) -> whrec c stack + | x -> x,stack + in + whrec + +(* whd flattens embedded applications + (whd_castapp ((((a b) c d) e f g) h)) -> (a b c d e f g h) + even if some casts exist in ((((a b) c d) e f g) h)) + *) +let whd_castapp x = applist(whd_castapp_stack x []) + + +(***************************************) +(* alpha and eta conversion functions *) +(***************************************) + +(* alpha conversion : ignore print names and casts *) +let rec eq_constr_rec m n = + if m = n then true else + match (strip_head_cast m,strip_head_cast n) with + | (DOP2(Cast,c1,_),c2) -> eq_constr_rec c1 c2 + | (c1,DOP2(Cast,c2,_)) -> eq_constr_rec c1 c2 + | (Rel p1,Rel p2) -> p1=p2 + | (DOPN(oper1,cl1),DOPN(oper2,cl2)) -> + oper1=oper2 & array_for_all2 eq_constr_rec cl1 cl2 + | (DOP0 oper1,DOP0 oper2) -> oper1=oper2 + | (DOP1(i,c1),DOP1(j,c2)) -> (i=j) & eq_constr_rec c1 c2 + | (DOP2(i,c1,c1'),DOP2(j,c2,c2')) -> + (i=j) & eq_constr_rec c1 c2 & eq_constr_rec c1' c2' + | (DLAM(_,c1),DLAM(_,c2)) -> eq_constr_rec c1 c2 + | (DLAMV(_,cl1),DLAMV(_,cl2)) -> + array_for_all2 eq_constr_rec cl1 cl2 + | _ -> false + +let eq_constr = eq_constr_rec + +let rec eq_constr_with_meta_rec m n= + (m=n) or + (match (strip_head_cast m,strip_head_cast n) with + | (DOP2(Cast,c1,_),c2) -> eq_constr_rec c1 c2 + | (c1,DOP2(Cast,c2,_)) -> eq_constr_rec c1 c2 + | (Rel p1,Rel p2) -> p1=p2 + | (DOPN(oper1,cl1),DOPN(oper2,cl2)) -> + oper1=oper2 & array_for_all2 eq_constr_rec cl1 cl2 + | (DOP0 oper1,DOP0 oper2) -> oper1=oper2 + | (DOP1(i,c1),DOP1(j,c2)) -> (i=j) & eq_constr_rec c1 c2 + | (DOP2(i,c1,c1'),DOP2(j,c2,c2')) -> + (i=j) & eq_constr_rec c1 c2 & eq_constr_rec c1' c2' + | (DLAM(_,c1),DLAM(_,c2)) -> eq_constr_rec c1 c2 + | (DLAMV(_,cl1),DLAMV(_,cl2)) -> + array_for_all2 eq_constr_rec cl1 cl2 + | _ -> false) + +(* On reduit une serie d'eta-redex de tete ou rien du tout *) +(* [x1:c1;...;xn:cn]@(f;a1...an;x1;...;xn) --> @(f;a1...an) *) +(* Remplace 2 versions précédentes buggées *) + +let rec eta_reduce_head c = + match c with + | DOP2(Lambda,c1,DLAM(_,c')) -> + (match eta_reduce_head c' with + | DOPN(AppL,cl) -> + let lastn = (Array.length cl) - 1 in + if lastn < 1 then anomaly "application without arguments" + else + (match cl.(lastn) with + | Rel 1 -> + let c' = + if lastn = 1 then cl.(0) + else DOPN(AppL,Array.sub cl 0 lastn) + in + if (not ((dependent (Rel 1) c'))) + then lift (-1) c' + else c + | _ -> c) + | _ -> c) + | _ -> c + +(* alpha-eta conversion : ignore print names and casts *) + +let rec eta_eq_constr t1 t2 = + let t1 = eta_reduce_head (strip_head_cast t1) + and t2 = eta_reduce_head (strip_head_cast t2) in + t1=t2 or match (t1,t2) with + | (DOP2(Cast,c1,_),c2) -> eta_eq_constr c1 c2 + | (c1,DOP2(Cast,c2,_)) -> eta_eq_constr c1 c2 + | (Rel p1,Rel p2) -> p1=p2 + | (DOPN(oper1,cl1),DOPN(oper2,cl2)) -> + oper1=oper2 & array_for_all2 eta_eq_constr cl1 cl2 + | (DOP0 oper1,DOP0 oper2) -> oper1=oper2 + | (DOP1(i,c1),DOP1(j,c2)) -> (i=j) & eta_eq_constr c1 c2 + | (DOP2(i,c1,c1'),DOP2(j,c2,c2')) -> + (i=j) & eta_eq_constr c1 c2 & eta_eq_constr c1' c2' + | (DLAM(_,c1),DLAM(_,c2)) -> eta_eq_constr c1 c2 + | (DLAMV(_,cl1),DLAMV(_,cl2)) -> array_for_all2 eta_eq_constr cl1 cl2 + | _ -> false + + +(* This renames bound variablew with fresh and distinct names *) +(* in such a way that the printer doe not generate new names *) +(* and therefore that printed names are the intern names *) +(* In this way, tactics such as Induction works well *) + +let rec rename_bound_var l = function + | DOP2(Prod,c1,DLAM(Name(s),c2)) -> + if dependent (Rel 1) c2 then + let s' = next_ident_away s (global_vars c2@l) in + DOP2(Prod,c1,DLAM(Name(s'),rename_bound_var (s'::l) c2)) + else + DOP2(Prod,c1,DLAM(Name(s),rename_bound_var l c2)) + | DOP2(Prod,c1,DLAM(Anonymous,c2)) -> + DOP2(Prod,c1,DLAM(Anonymous,rename_bound_var l c2)) + | DOP2(Cast,c,t) -> DOP2(Cast,rename_bound_var l c,t) + | x -> x + +(***************************) +(* substitution functions *) +(***************************) + +(* First utilities for avoiding telescope computation for subst_term *) + +let prefix_application k (c:constr) (t:constr) = + match (whd_castapp c,whd_castapp t) with + | ((DOPN(AppL,cl1)),DOPN(AppL,cl2)) -> + let l1 = Array.length cl1 + and l2 = Array.length cl2 in + if l1 <= l2 + && eq_constr (DOPN(AppL,cl1)) (DOPN(AppL,Array.sub cl2 0 l1)) then + Some(DOPN(AppL, array_cons (Rel k) (Array.sub cl2 l1 (l2 - l1)))) + else + None + | (_,_) -> None + +let prefix_application_eta k (c:constr) (t:constr) = + match (whd_castapp c,whd_castapp t) with + | ((DOPN(AppL,cl1)),DOPN(AppL,cl2)) -> + let l1 = Array.length cl1 + and l2 = Array.length cl2 in + if l1 <= l2 && + eta_eq_constr (DOPN(AppL,cl1)) (DOPN(AppL,Array.sub cl2 0 l1)) then + Some(DOPN(AppL,array_cons (Rel k) (Array.sub cl2 l1 (l2 - l1)))) + else + None + | (_,_) -> None + +(* Used in trad and progmach *) +let rec rename_rels curidx sofar = function + | [] -> sofar + | ((id,Rel n)::tl as l) -> + if curidx = n then + rename_rels (curidx+1) (subst1 (VAR id) sofar) tl + else + rename_rels (curidx+1) (subst1 (DOP0 Implicit) sofar) l + | _ -> assert false + +let sort_increasing_snd = + Sort.list + (fun x y -> match x,y with + (_,Rel m),(_,Rel n) -> m < n + | _ -> assert false) + +let clean_rhs rhs worklist = + let workvars = List.filter (compose isVAR snd) worklist in + let rhs' = + replace_vars + (List.map (fun (id',v) -> let id = destVar v in + (id,{sinfo=Closed; sit=VAR id'})) + workvars) + rhs + in + let workrels = List.filter (compose isRel snd) worklist in + let workrels' = sort_increasing_snd workrels in + rename_rels 1 rhs' workrels' + +(* Recognizing occurrences of a given subterm in a term for Pattern : + (subst_term c t) substitutes (Rel 1) for all occurrences of term c + in a (closed) term t *) + +let subst_term c t = + let rec substrec k c t = + match prefix_application k c t with + | Some x -> x + | None -> + (if eq_constr t c then Rel(k) else match t with + | DOPN(Const sp,cl) -> t + | DOPN(MutInd (x_0,x_1),cl) -> t + | DOPN(MutConstruct (x_0,x_1),cl) -> t + | DOPN(oper,tl) -> DOPN(oper,Array.map (substrec k c) tl) + | DOP1(i,t) -> DOP1(i,substrec k c t) + | DOP2(oper,c1,c2) -> DOP2(oper,substrec k c c1,substrec k c c2) + | DLAM(na,t) -> DLAM(na,substrec (k+1) (lift 1 c) t) + | DLAMV(na,v) -> DLAMV(na,Array.map (substrec (k+1) (lift 1 c)) v) + | _ -> t) + in + substrec 1 c t + +(* same as subst_term, but modulo eta *) + +let subst_term_eta_eq c t = + let rec substrec k c t = + match prefix_application_eta k c t with + | Some x -> x + | None -> + (if eta_eq_constr t c then Rel(k) else match t with + | DOPN(Const sp,cl) -> t + | DOPN(oper,tl) -> DOPN(oper,Array.map (substrec k c) tl) + | DOP1(i,t) -> DOP1(i,substrec k c t) + | DOP2(oper,c1,c2) -> DOP2(oper,substrec k c c1,substrec k c c2) + | DLAM(na,t) -> DLAM(na,substrec (k+1) (lift 1 c) t) + | DLAMV(na,v)-> DLAMV(na,Array.map (substrec (k+1) (lift 1 c)) v) + | _ -> t) + in + substrec 1 c t + +(* bl : (int,constr) Listmap.t = (int * constr) list *) +(* c : constr *) +(* for each binding (i,c_i) in bl, substitutes the metavar i by c_i in c *) +(* Raises Not_found if c contains a meta that is not in the association list *) + +let rec subst_meta bl c = + match c with + | DOP0(Meta(i)) -> List.assoc i bl + | DOP1(op,c') -> DOP1(op, subst_meta bl c') + | DOP2(op,c'1, c'2) -> DOP2(op, subst_meta bl c'1, subst_meta bl c'2) + | DOPN(op, c') -> DOPN(op, Array.map (subst_meta bl) c') + | _ -> c + +(***************************) +(* occurs check functions *) +(***************************) + +let rec occur_meta = function + | DOP2(Prod,t,DLAM(_,c)) -> (occur_meta t) or (occur_meta c) + | DOP2(Lambda,t,DLAM(_,c)) -> (occur_meta t) or (occur_meta c) + | DOPN(_,cl) -> (array_exists occur_meta cl) + | DOP2(Cast,c,t) -> occur_meta c or occur_meta t + | DOP0(Meta(_)) -> true + | _ -> false + +let rel_vect = (Generic.rel_vect : int -> int -> constr array) + +(* Transforms a constr into a matchable constr*) +let rec matchable=function + | DOP1(op,t) -> + DOP1(op,matchable t) + | DOP2(op,t1,t2) -> + DOP2(op,matchable t1,matchable t2) + | DOPN(op,tab) -> + (match op with + | MutInd(sp,rk) -> + DOPL(XTRA("IT",[Coqast.Id((rk,0),string_of_path sp)]), + Array.to_list (Array.map matchable tab)) + | MutConstruct((sp,rkt),rkc) -> + DOPL(XTRA("IC",[Coqast.Id((rkt,rkc),string_of_path sp)]), + Array.to_list (Array.map matchable tab)) + | Const sp -> + DOPL(XTRA("C",[Coqast.Id((0,0),string_of_path sp)]), + Array.to_list (Array.map matchable tab)) + | a -> + DOPL(a,Array.to_list (Array.map matchable tab))) + | DOPL(op,lst) -> + DOPL(op,List.map matchable lst) + | DLAM(ne,t) -> + DLAM(ne,matchable t) + | DLAMV(ne,tab) -> + DLAMV(ne,(Array.map matchable tab)) + | a -> a + +let rec unmatchable=function + | DOP1(op,t) -> + DOP1(op,unmatchable t) + | DOP2(op,t1,t2) -> + DOP2(op,unmatchable t1,unmatchable t2) + | DOPN(op,tab) -> + DOPN(op,Array.map unmatchable tab) + | DOPL(op,lst) -> + (match op with + | XTRA("IT",[Coqast.Id((rk,0),str)]) -> + DOPN(MutInd(path_of_string str,rk), + Array.of_list (List.map unmatchable lst)) + | XTRA("IC",[Coqast.Id((rkt,rkc),str)]) -> + DOPN(MutConstruct((path_of_string str,rkt),rkc), + Array.of_list (List.map unmatchable lst)) + | XTRA("C",[Coqast.Id((0,0),str)]) -> + DOPN(Const(path_of_string str), + Array.of_list (List.map unmatchable lst)) + | a -> + DOPN(a,Array.of_list (List.map unmatchable lst))) + | DLAM(ne,t) -> + DLAM(ne,unmatchable t) + | DLAMV(ne,tab) -> + DLAMV(ne,(Array.map unmatchable tab)) + | a -> a + +(***************************) +(* hash-consing functions *) +(***************************) + +module Hsorts = + Hashcons.Make( + struct + type t = sorts + type u = section_path -> section_path + let hash_sub hsp = function + | Prop c -> Prop c + | Type {u_sp=sp; u_num=n} -> Type {u_sp=hsp sp; u_num=n} + let equal s1 s2 = + match (s1,s2) with + | (Prop c1, Prop c2) -> c1=c2 + | (Type {u_sp=sp1; u_num=n1}, Type {u_sp=sp2; u_num=n2}) -> + sp1==sp2 & n1=n2 + |_ -> false + let hash = Hashtbl.hash + end) + +module Hoper = + Hashcons.Make( + struct + type t = sorts oper + type u = (Coqast.t -> Coqast.t) * (sorts -> sorts) + * (section_path -> section_path) * (string -> string) + let hash_sub (hast,hsort,hsp,hstr) = function + | XTRA(s,al) -> XTRA(hstr s, List.map hast al) + | Sort s -> Sort (hsort s) + | Const sp -> Const (hsp sp) + | Abst sp -> Abst (hsp sp) + | MutInd (sp,i) -> MutInd (hsp sp, i) + | MutConstruct ((sp,i),j) -> MutConstruct ((hsp sp,i),j) + | MutCase(Some (sp,i)) -> MutCase(Some (hsp sp, i)) + | t -> t + let equal o1 o2 = + match (o1,o2) with + | (XTRA(s1,al1), XTRA(s2,al2)) -> + (s1==s2 & List.length al1 = List.length al2) + & List.for_all2 (==) al1 al2 + | (Sort s1, Sort s2) -> s1==s2 + | (Const sp1, Const sp2) -> sp1==sp2 + | (Abst sp1, Abst sp2) -> sp1==sp2 + | (MutInd (sp1,i1), MutInd (sp2,i2)) -> sp1==sp2 & i1=i2 + | (MutConstruct((sp1,i1),j1), MutConstruct((sp2,i2),j2)) -> + sp1==sp2 & i1=i2 & j1=j2 + | (MutCase(Some (sp1,i1)),MutCase(Some (sp2,i2))) -> sp1==sp2 & i1=i2 + | _ -> o1=o2 + let hash = Hashtbl.hash + end) + +module Hconstr = + Hashcons.Make( + struct + type t = constr + type u = (constr -> constr) + * ((sorts oper -> sorts oper) * (name -> name) + * (identifier -> identifier)) + let hash_sub = hash_term + let equal = comp_term + let hash = Hashtbl.hash + end) + +let hcons_oper (hast,hsorts,hsp,hstr) = + Hashcons.simple_hcons Hoper.f (hast,hsorts,hsp,hstr) + +let hcons_term (hast,hsorts,hsp,hname,hident,hstr) = + let hoper = hcons_oper (hast,hsorts,hsp,hstr) in + Hashcons.recursive_hcons Hconstr.f (hoper,hname,hident) + +module Htype = + Hashcons.Make( + struct + type t = type_judgment + type u = (constr -> constr) * (sorts -> sorts) + let hash_sub (hc,hs) j = {body=hc j.body; typ=hs j.typ} + let equal j1 j2 = j1.body==j2.body & j1.typ==j2.typ + let hash = Hashtbl.hash + end) + +let hcons_constr (hspcci,hspfw,hname,hident,hstr) = + let hsortscci = Hashcons.simple_hcons Hsorts.f hspcci in + let hsortsfw = Hashcons.simple_hcons Hsorts.f hspfw in + let (hast,_) = Coqast.hcons_ast hstr in + let hcci = hcons_term (hast,hsortscci,hspcci,hname,hident,hstr) in + let hfw = hcons_term (hast,hsortsfw,hspfw,hname,hident,hstr) in + let htcci = Hashcons.simple_hcons Htype.f (hcci,hsortscci) in + (hcci,hfw,htcci) + +let hcons1_constr c = + let hnames = hcons_names() in + let (hc,_,_) = hcons_constr hnames in + hc c + +(* Puts off the casts *) +let put_off_casts = strip_outer_cast + +(*Verifies if the constr has an head constant*) +let is_hd_const=function + | DOPN(AppL,t) -> + (match (t.(0)) with + | DOPN(Const c,_) -> + Some (Const c,Array.of_list (List.tl (Array.to_list t))) + |_ -> None) + |_ -> None + +(*Gives the occurences number of t in u*) +let rec nb_occ_term t u= + let one_step t=function + | DOP1(_,c) -> nb_occ_term t c + | DOP2(_,c0,c1) -> (nb_occ_term t c0)+(nb_occ_term t c1) + | DOPN(_,a) -> Array.fold_left (fun a x -> a+(nb_occ_term t x)) 0 a + | DOPL(_,l) -> List.fold_left (fun a x -> a+(nb_occ_term t x)) 0 l + | DLAM(_,c) -> nb_occ_term t c + | DLAMV(_,a) -> Array.fold_left (fun a x -> a+(nb_occ_term t x)) 0 a + | _ -> 0 + in + if t=u then + 1 + else + one_step t u + +(*Alpha-conversion*) +let bind_eq=function + | (Anonymous,Anonymous) -> true + | (Name _,Name _) -> true + | _ -> false + + (*Tells if two constrs are equal modulo unification*) +let rec eq_mod_rel l_meta=function + | (t,DOP0(Meta n)) -> + if not(List.mem n (fst (List.split l_meta))) then + Some ([(n,t)]@l_meta) + else if (List.assoc n l_meta)=t then + Some l_meta + else + None + | DOP1(op0,c0), DOP1(op1,c1) -> + if op0=op1 then + eq_mod_rel l_meta (c0,c1) + else + None + | DOP2(op0,t0,c0), DOP2(op1,t1,c1) -> + if op0=op1 then + match (eq_mod_rel l_meta (t0,t1)) with + | None -> None + | Some l -> eq_mod_rel l (c0,c1) + else + None + | DOPN(op0,t0), DOPN(op1,t1) -> + if (op0=op1) & ((Array.length t0)=(Array.length t1)) then + List.fold_left2 + (fun a c1 c2 -> + match a with + | None -> None + | Some l -> eq_mod_rel l (c1,c2)) (Some l_meta) + (Array.to_list t0) (Array.to_list t1) + else + None + | DLAM(n0,t0),DLAM(n1,t1) -> + if (bind_eq (n0,n1)) then + eq_mod_rel l_meta (t0,t1) + else + None + | (t,u) -> + if t=u then Some l_meta else None + +(*Substitutes a list of meta l in t*) +let rec subst_with_lmeta l=function + | DOP0(Meta n) -> List.assoc n l + | DOP1(op,t) -> DOP1(op,subst_with_lmeta l t) + | DOP2(op,t0,t1) -> DOP2(op,subst_with_lmeta l t0,subst_with_lmeta l t1) + | DOPN(op,t) -> DOPN(op,Array.map (subst_with_lmeta l) t) + | DOPL(op,ld) -> DOPL(op,List.map (subst_with_lmeta l) ld) + | DLAM(n,t) -> DLAM(n,subst_with_lmeta l t) + | DLAMV(n,t) -> DLAMV(n,Array.map (subst_with_lmeta l) t) + | t -> t + +(*Carries out the following translation: DOPN(AppL,[|t|]) -> t and + DOPN(AppL,[|DOPN(AppL,t);...;t'|]) -> DOPN(AppL;[|t;...;t'|])*) +let rec appl_elim=function + | DOPN(AppL,t) -> + if (Array.length t)=1 then + appl_elim t.(0) + else + (match t.(0) with + | DOPN(AppL,t') -> + appl_elim (DOPN(AppL,Array.append t' + (Array.of_list + (List.tl (Array.to_list t))))) + |_ -> DOPN(AppL,Array.map appl_elim t)) + | DOP1(op,t) -> DOP1(op,appl_elim t) + | DOP2(op,t0,t1) -> DOP2(op,appl_elim t0,appl_elim t1) + | DOPN(op,t) -> DOPN(op,Array.map appl_elim t) + | DOPL(op,ld) -> DOPL(op,List.map appl_elim ld) + | DLAM(n,t) -> DLAM(n,appl_elim t) + | DLAMV(n,t) -> DLAMV(n,Array.map appl_elim t) + | t -> t + +(*Gives Some(first instance of ceq in cref,occurence number for this + instance) or None if no instance of ceq can be found in cref*) +let sub_term_with_unif cref ceq= + let rec find_match l_meta nb_occ op_ceq t_eq=function + | DOPN(AppL,t) as u -> + (match (t.(0)) with + | DOPN(op,t_op) -> + let t_args=Array.of_list (List.tl (Array.to_list t)) in + if op=op_ceq then + match + (List.fold_left2 + (fun a c0 c1 -> + match a with + | None -> None + | Some l -> eq_mod_rel l (c0,c1)) (Some l_meta) + (Array.to_list t_args) (Array.to_list t_eq)) + with + | None -> + List.fold_left + (fun (l_meta,nb_occ) x -> find_match l_meta nb_occ + op_ceq t_eq x) (l_meta,nb_occ) (Array.to_list + t_args) + | Some l -> (l,nb_occ+1) + else + List.fold_left + (fun (l_meta,nb_occ) x -> find_match l_meta + nb_occ op_ceq t_eq x) + (l_meta,nb_occ) (Array.to_list t) + | VAR _ -> + List.fold_left + (fun (l_meta,nb_occ) x -> find_match l_meta + nb_occ op_ceq t_eq x) + (l_meta,nb_occ) (Array.to_list t) + |_ -> (l_meta,nb_occ)) + | DOP2(_,t,DLAM(_,c)) -> + let (lt,nbt)=find_match l_meta nb_occ op_ceq t_eq t in + find_match lt nbt op_ceq t_eq c + | DOPN(_,t) -> + List.fold_left + (fun (l_meta,nb_occ) x -> find_match l_meta nb_occ op_ceq t_eq x) + (l_meta,nb_occ) (Array.to_list t) + |_ -> (l_meta,nb_occ) + in + match (is_hd_const ceq) with + | None -> + if (occur_meta ceq) then + None + else + let nb_occ=nb_occ_term ceq cref in + if nb_occ=0 then + None + else + Some (ceq,nb_occ) + | Some (head,t_args) -> + let (l,nb)=find_match [] 0 head t_args cref in + if nb=0 then + None + else + Some ((subst_with_lmeta l ceq),nb) diff --git a/kernel/term.mli b/kernel/term.mli new file mode 100644 index 0000000000..d5a9b11d35 --- /dev/null +++ b/kernel/term.mli @@ -0,0 +1,520 @@ + +(* $Id$ *) + +open Names +open Generic + +(* The Type of Constructions Terms. *) + +(* Coq abstract syntax with deBruijn variables; 'a is the type of sorts *) + +type 'a oper = + (* DOP0 *) + | Meta of int + | Sort of 'a + | Implicit + (* DOP2 *) + | Cast | Prod | Lambda + (* DOPN *) + | AppL | Const of section_path | Abst of section_path + | MutInd of section_path * int + | MutConstruct of (section_path * int) * int + | MutCase of case_info + | Fix of int array * int + | CoFix of int + + | XTRA of string * Coqast.t list + (* an extra slot, for putting in whatever sort of + operator we need for whatever sort of application *) + +and case_info = (section_path * int) option + +type contents = Pos | Null + +val str_of_contents : contents -> string +val contents_of_str : string -> contents + +type sorts = + | Prop of contents (* Prop and Set *) + | Type of Univ.universe (* Type *) + +val mk_Set : sorts +val mk_Prop : sorts + +type constr = sorts oper term + +type 'a judge = { body : constr; typ : 'a } + +type type_judgment = sorts judge +type term_judgment = type_judgment judge + +type conv_pb = CONV | CONV_LEQ | CONV_X | CONV_X_LEQ + + +(****************************************************************************) +(* Functions for dealing with constr terms *) +(****************************************************************************) + +(* The following functions are intended to simplify and to uniform the + manipulation of terms. Some of these functions may be overlapped with + previous ones. *) + +(* Concrete type for making pattern-matching *) + +type kindOfTerm = + | IsRel of int + | IsMeta of int + | IsVar of identifier + | IsXtra of string * Coqast.t list + | IsSort of sorts + | IsImplicit + | IsCast of constr * constr + | IsProd of name * constr * constr + | IsLambda of name * constr * constr + | IsAppL of constr array + | IsConst of section_path * constr array + | IsAbst of section_path * constr array + | IsMutInd of section_path * int * constr array + | IsMutConstruct of section_path * int * int * constr array + | IsMutCase of case_info * constr * constr * constr array + | IsFix of int array * int * constr array * name list * + constr array + | IsCoFix of int * constr array * name list * constr array + +(* Discriminates which kind of term is it. + Note that there is no cases for [[DLAM] and [DLAMV]. These terms do not + make sense alone, but they must be preceeded by the application of + an operator. +*) + +val kind_of_term : constr -> kindOfTerm + +(*********************) +(* Term constructors *) +(*********************) + +(* Constructs a DeBrujin index *) +val mkRel : int -> constr + +(* Constructs an existential variable named "?" *) +val mkExistential : constr + +(* Constructs an existential variable named "?n" *) +val mkMeta : int -> constr + +(* Constructs a Variable *) +val mkVar : identifier -> constr + +(* Construct an XTRA term (XTRA is an extra slot for whatever you want) *) +val mkXtra : string -> Coqast.t list -> constr + +(* Construct a type *) +val mkSort : sorts -> constr +val mkProp : constr +val mkSet : constr +val mkType : Univ.universe -> constr +val prop : sorts +val spec : sorts +val types : sorts +val type_0 : sorts +val type_1 : sorts + +(* Construct an implicit (see implicit arguments in the RefMan) *) +(* Used for extraction *) +val mkImplicit : constr +val implicit_sort : sorts + +(* 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) *) +val mkCast : constr -> constr -> constr + +(* Constructs the product (x:t1)t2 -- x may be anonymous *) +val mkProd : name -> constr -> constr -> constr + +(* non-dependant product t1 -> t2 *) +val mkArrow : constr -> constr -> constr + +(* named product *) +val mkNamedProd : identifier -> constr -> constr -> constr + +(* Constructs the abstraction [x:t1]t2 *) +val mkLambda : name -> constr -> constr -> constr +val mkNamedLambda : identifier -> constr -> constr -> constr + +(* If a = [| t1; ...; tn |], constructs the application (t1 ... tn) *) +val mkAppL : constr array -> constr +val mkAppList : constr list -> constr + +(* Constructs a constant *) +(* The array of terms correspond to the variables introduced in the section *) +val mkConst : section_path -> constr array -> constr + +(* Constructs an abstract object *) +val mkAbst : section_path -> constr array -> constr + +(* Constructs the ith (co)inductive type of the block named sp *) +(* The array of terms correspond to the variables introduced in the section *) +val mkMutInd : section_path -> int -> constr array -> constr + +(* Constructs the jth constructor of the ith (co)inductive type of the + block named sp. The array of terms correspond to the variables + introduced in the section *) +val mkMutConstruct : section_path -> int -> int -> constr array -> constr + +(* Constructs the term <p>Case c of c1 | c2 .. | cn end *) +val mkMutCase : case_info -> constr -> constr -> constr list -> constr +val mkMutCaseA : case_info -> constr -> constr -> constr array -> constr + +(* If recindxs = [|i1,...in|] + typarray = [|t1,...tn|] + funnames = [f1,.....fn] + bodies = [b1,.....bn] + then + + mkFix recindxs i typarray funnames bodies + + constructs the ith function of the block + + Fixpoint f1 [ctx1] = b1 + with f2 [ctx2] = b2 + ... + with fn [ctxn] = bn. + + where the lenght of the jth context is ij. +*) +val mkFix : int array -> int -> type_judgment array -> name list + -> constr array -> constr + +(* Similarly, but we assume the body already constructed *) +val mkFixDlam : int array -> int -> type_judgment array + -> constr array -> constr + +(* If typarray = [|t1,...tn|] + funnames = [f1,.....fn] + bodies = [b1,.....bn] + then + + mkCoFix i typsarray funnames bodies + + constructs the ith function of the block + + CoFixpoint f1 = b1 + with f2 = b2 + ... + with fn = bn. + +*) +val mkCoFix : int -> type_judgment array -> name list + -> constr array -> constr + +(* Similarly, but we assume the body already constructed *) +val mkCoFixDlam : int -> type_judgment array -> constr array -> constr + +(********************) +(* Term destructors *) +(********************) + +(* Destructor operations : partial functions + Raise invalid_arg "dest*" if the const has not the expected form *) + +(* Destructs a DeBrujin index *) +val destRel : constr -> int + +(* Destructs an existential variable *) +val destMeta : constr -> int +val isMETA : constr -> bool + +(* Destructs a variable *) +val destVar : constr -> identifier + +(* Destructs an XTRA *) +val destXtra : constr -> string * Coqast.t list + +(* Destructs a sort *) +val destSort : constr -> sorts +val contents_of_kind : constr -> contents +val is_Prop : constr -> bool (* true for Prop *) +val is_Set : constr -> bool (* true for Set *) +val isprop : constr -> bool (* true for DOP0 (Sort (Prop _)) *) +val is_Type : constr -> bool (* true for DOP0 (Sort (Type _)) *) +val iskind : constr -> bool (* true for Prop, Set and Type(_) *) + +val isType : sorts -> bool (* true for Type(_) *) +val is_small : sorts -> bool (* true for Prop and Set *) + +(* Destructs a casted term *) +val destCast : constr -> constr * constr +val cast_type : constr -> constr (* 2nd proj *) +val cast_term : constr -> constr (* 1st proj *) +val isCast : constr -> bool +(* removes recursively the casts around a term *) +(* strip_outer_cast (Cast (Cast ... (Cast c, t) ... )) is c *) +val strip_outer_cast : constr -> constr + +(* Destructs the product (x:t1)t2 *) +val destProd : constr -> name * constr * constr +val hd_of_prod : constr -> constr +val hd_is_constructor : constr -> bool + +(* Destructs the abstraction [x:t1]t2 *) +val destLambda : constr -> name * constr * constr + +(* Destructs an application *) +val destAppL : constr -> constr array +val isAppL : constr -> bool +val hd_app : constr -> constr +val args_app : constr -> constr array + +(* Destructs a constant *) +val destConst : constr -> section_path * constr array +val path_of_const : constr -> section_path +val args_of_const : constr -> constr array + +(* Destrucy an abstract term *) +val destAbst : constr -> section_path * constr array +val path_of_abst : constr -> section_path +val args_of_abst : constr -> constr array + +(* Destructs a (co)inductive type *) +val destMutInd : constr -> section_path * int * constr array +val op_of_mind : constr -> section_path * int +val args_of_mind : constr -> constr array +val ci_of_mind : constr -> case_info + +(* Destructs a constructor *) +val destMutConstruct : constr -> section_path * int * int * constr array +val op_of_mconstr : constr -> (section_path * int) * int +val args_of_mconstr : constr -> constr array + +(* Destructs a term <p>Case c of lc1 | lc2 .. | lcn end *) +val destCase : constr -> case_info * constr * constr * constr array + +(* Destructs the ith function of the block + Fixpoint f1 [ctx1] = b1 + with f2 [ctx2] = b2 + ... + with fn [ctxn] = bn. + + where the lenght of the jth context is ij. +*) +val destGralFix : constr array -> constr array * Names.name list + * constr array +val destFix : constr -> int array * int * type_judgment array + * Names.name list * constr array +val destCoFix : constr -> int * type_judgment array * Names.name list + * constr array + +(* Provisoire, le temps de maitriser les cast *) +val destUntypedFix : constr -> int array * int * constr array + * Names.name list * constr array +val destUntypedCoFix : constr -> int * constr array * Names.name list + * constr array + +(***********************************) +(* Other term constructors *) +(***********************************) + +val abs_implicit : constr -> constr +val lambda_implicit : constr -> constr +val lambda_implicit_lift : int -> constr -> constr + +val applist : constr * constr list -> constr +val applistc : constr -> constr list -> constr +val appvect : constr * constr array -> constr +val appvectc : constr -> constr array -> constr +(* prodn n ([x1:T1]..[xn:Tn]Gamma) b = (x1:T1)..(xn:Tn)b *) +val prodn : int -> (name * constr) list -> constr -> constr +(* lamn n ([x1:T1]..[xn:T]Gamma) b = [x1:T1]..[xn:Tn]b *) +val lamn : int -> (name * constr) list -> constr -> constr + +(* prod_it b [x1:T1;..xn:Tn] = (x1:T1)..(xn:Tn)b *) +val prod_it : constr -> (name * constr) list -> constr +(* lam_it b [x1:T1;..xn:Tn] = [x1:T1]..[xn:Tn]b *) +val lam_it : constr -> (name * constr) list -> constr + + +(* to_lambda n (x1:T1)...(xn:Tn)(xn+1:Tn+1)...(xn+j:Tn+j)T = + [x1:T1]...[xn:Tn](xn+1:Tn+1)...(xn+j:Tn+j)T *) +val to_lambda : int -> constr -> constr +val to_prod : int -> constr -> constr + +(*********************************) +(* Other term destructors *) +(*********************************) + +(* Transforms a product term (x1:T1)..(xn:Tn)T into the pair + ([(xn,Tn);...;(x1,T1)],T), where T is not a product *) +val decompose_prod : constr -> (name*constr) list * constr + +(* Transforms a lambda term [x1:T1]..[xn:Tn]T into the pair + ([(xn,Tn);...;(x1,T1)],T), where T is not a lambda *) +val decompose_lam : constr -> (name*constr) list * constr + +(* Given a positive integer n, transforms a product term (x1:T1)..(xn:Tn)T + into the pair ([(xn,Tn);...;(x1,T1)],T) *) +val decompose_prod_n : int -> constr -> (name*constr) list * constr + +(* Given a positive integer n, transforms a lambda term [x1:T1]..[xn:Tn]T + into the pair ([(xn,Tn);...;(x1,T1)],T) *) +val decompose_lam_n : int -> constr -> (name*constr) list * constr + +(* (nb_lam [na1:T1]...[nan:Tan]c) where c is not an abstraction + * gives n (casts are ignored) *) +val nb_lam : constr -> int + +(* similar to nb_lam, but gives the number of products instead *) +val nb_prod : constr -> int + +(********************************************************************) +(* various utility functions for implementing terms with bindings *) +(********************************************************************) + +val extract_lifted : int * constr -> constr +val insert_lifted : constr -> int * constr + +(* l is a list of pairs (n:nat,x:constr), env is a stack of (na:name,T:constr) + push_and_lift adds a component to env and lifts l one step *) +val push_and_lift : + name * constr -> (name * constr) list -> (int * constr) list + -> (name * constr) list * (int * constr) list + +(* if T is not (x1:A1)(x2:A2)....(xn:An)T' then (push_and_liftl n env T l) + raises an error else it gives ([x1,A1 ; x2,A2 ; ... ; xn,An]@env,T',l') + where l' is l lifted n steps *) +val push_and_liftl : + int -> (name * constr) list -> constr -> (int * constr) list + -> (name * constr) list * constr * (int * constr) list + +(* if T is not [x1:A1][x2:A2]....[xn:An]T' then (push_lam_and_liftl n env T l) + raises an error else it gives ([x1,A1 ; x2,A2 ; ... ; xn,An]@env,T',l') + where l' is l lifted n steps *) +val push_lam_and_liftl : + int -> (name * constr) list -> constr -> (int * constr) list + -> (name * constr) list * constr * (int * constr) list + +(* l is a list of pairs (n:nat,x:constr), tlenv is a stack of +(na:name,T:constr), B : constr, na : name +(prod_and_pop ((na,T)::tlenv) B l) gives (tlenv, (na:T)B, l') +where l' is l lifted down one step *) +val prod_and_pop : + (name * constr) list -> constr -> (int * constr) list + -> (name * constr) list * constr * (int * constr) list + +(* recusively applies prod_and_pop : +if env = [na1:T1 ; na2:T2 ; ... ; nan:Tn]@tlenv +then +(prod_and_popl n env T l) gives (tlenv,(nan:Tn)...(na1:Ta1)T,l') where +l' is l lifted down n steps *) +val prod_and_popl : + int -> (name * constr) list -> constr -> (int * constr) list + -> (name * constr) list * constr * (int * constr) list + +(* similar to prod_and_pop, but gives [na:T]B intead of (na:T)B *) +val lam_and_pop : + (name * constr) list -> constr -> (int * constr) list + -> (name * constr) list * constr * (int * constr) list + +(* similar to prod_and_popl but gives [nan:Tan]...[na1:Ta1]B instead of + * (nan:Tan)...(na1:Ta1)B *) +val lam_and_popl : + int -> (name * constr) list -> constr -> (int * constr) list + -> (name * constr) list * constr * (int * constr) list + +(* similar to lamn_and_pop but generates new names whenever the name is + * Anonymous *) +val lam_and_pop_named : + (name * constr) list -> constr ->(int * constr) list ->identifier list + -> (name * constr) list * constr * (int * constr) list * identifier list + +(* similar to prod_and_popl but gives [nan:Tan]...[na1:Ta1]B instead of + * but it generates names whenever nai=Anonymous *) +val lam_and_popl_named : + int -> (name * constr) list -> constr -> (int * constr) list + -> (name * constr) list * constr * (int * constr) list +(* [lambda_ize n T endpt] + * will pop off the first n products in T, then stick in endpt, + * properly lifted, and then push back the products, but as lambda- + * abstractions + *) +val lambda_ize :int ->'a oper term -> 'a oper term -> 'a oper term + +(******************************************************************) +(* Flattening and unflattening of embedded applications and casts *) +(******************************************************************) + +(* if c is not an AppL, it is transformed into mkAppL [| c |] *) +val ensure_appl : constr -> constr + +(* unflattens application lists *) +val telescope_appl : constr -> constr +(* flattens application lists *) +val collapse_appl : constr -> constr +val decomp_app : constr -> constr * constr list + + +(********************************************) +(* Misc functions on terms, judgments, etc *) +(********************************************) + +(* Level comparison for information extraction : Prop <= Type *) +val same_kind : constr -> constr -> bool +val le_kind : constr -> constr -> bool +val le_kind_implicit : constr -> constr -> bool + +val pb_is_univ_adjust : conv_pb -> bool +val pb_is_equal : conv_pb -> bool +val pb_equal : conv_pb -> conv_pb +val sort_hdchar : sorts -> string +(* val sort_cmp : conv_pb -> sorts -> sorts -> bool *) + + +(***************************) +(* occurs check functions *) +(***************************) +val occur_meta : constr -> bool +val rel_vect : int -> int -> constr array + +(* (occur_const (s:section_path) c) -> true if constant s occurs in c, + * false otherwise *) +val occur_const : section_path -> constr -> bool + +(* strips head casts and flattens head applications *) +val strip_head_cast : constr -> constr +val whd_castapp_stack : constr -> constr list -> constr * constr list +val whd_castapp : constr -> constr +val rename_bound_var : identifier list -> constr -> constr +val eta_reduce_head : constr -> constr +val eq_constr : constr -> constr -> bool +val eta_eq_constr : constr -> constr -> bool +val rename_rels : int -> constr -> (identifier * constr) list -> constr +val clean_rhs : constr -> (identifier * constr) list -> constr +val subst_term : constr -> constr -> constr +val subst_term_eta_eq : constr -> constr -> constr +val replace_consts : + (section_path * (identifier list * constr) option) list -> constr -> constr + +(* bl : (int,constr) Listmap.t = (int * constr) list *) +(* c : constr *) +(* for each binding (i,c_i) in bl, substitutes the metavar i by c_i in c *) +(* Raises Not_found if c contains a meta that is not in the association list *) + +val subst_meta : (int * constr) list -> constr -> constr + +(* Transforms a constr into a matchable constr *) +val matchable : constr -> constr +val unmatchable: constr -> constr + +(* New hash-cons functions *) + +val hcons_constr: + (section_path -> section_path) * + (section_path -> section_path) * + (name -> name) * + (identifier -> identifier) * + (string -> string) + -> + (constr -> constr) * + (constr -> constr) * + (type_judgment -> type_judgment) + +val hcons1_constr : constr -> constr diff --git a/kernel/univ.mli b/kernel/univ.mli new file mode 100644 index 0000000000..0bfaddbcc5 --- /dev/null +++ b/kernel/univ.mli @@ -0,0 +1,12 @@ + +(* $Id$ *) + +open Names + +type universe = { u_sp : section_path; u_num : int } + +val dummy_univ : universe + +val prop_univ : universe +val prop_univ_univ : universe +val prop_univ_univ_univ : universe |