From a0cfa4f118023d35b767a999d5a2ac4b082857b4 Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@debian.org>
Date: Fri, 25 Jul 2008 15:12:53 +0200
Subject: Imported Upstream version 8.2~beta3+dfsg

---
 checker/term.ml | 462 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 462 insertions(+)
 create mode 100644 checker/term.ml

(limited to 'checker/term.ml')

diff --git a/checker/term.ml b/checker/term.ml
new file mode 100644
index 00000000..45568a59
--- /dev/null
+++ b/checker/term.ml
@@ -0,0 +1,462 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id: term.ml 10098 2007-08-27 11:41:08Z herbelin $ *)
+
+(* This module instantiates the structure of generic deBruijn terms to Coq *)
+
+open Util
+open Pp
+open Names
+open Univ
+open Esubst
+
+(* Coq abstract syntax with deBruijn variables; 'a is the type of sorts *)
+
+type existential_key = int
+type metavariable = int
+
+(* This defines the strategy to use for verifiying a Cast *)
+
+(* This defines Cases annotations *)
+type case_style = LetStyle | IfStyle | LetPatternStyle | MatchStyle |
+  RegularStyle
+type case_printing =
+  { ind_nargs : int; (* number of real args of the inductive type *)
+    style     : case_style }
+type case_info =
+  { ci_ind        : inductive;
+    ci_npar       : int;
+    ci_cstr_nargs : int array; (* number of real args of each constructor *)
+    ci_pp_info    : case_printing (* not interpreted by the kernel *)
+  }
+
+(* Sorts. *)
+
+type contents = Pos | Null
+
+type sorts =
+  | Prop of contents                      (* proposition types *)
+  | Type of universe
+
+type sorts_family = InProp | InSet | InType
+
+let family_of_sort = function
+  | Prop Null -> InProp
+  | Prop Pos -> InSet
+  | Type _ -> InType
+
+(********************************************************************)
+(*       Constructions as implemented                               *)
+(********************************************************************)
+
+(* [constr array] is an instance matching definitional [named_context] in
+   the same order (i.e. last argument first) *)
+type 'constr pexistential = existential_key * 'constr array
+type 'constr prec_declaration =
+    name array * 'constr array * 'constr array
+type 'constr pfixpoint =
+    (int array * int) * 'constr prec_declaration
+type 'constr pcofixpoint =
+    int * 'constr prec_declaration
+
+type cast_kind = VMcast | DEFAULTcast 
+
+(*s*******************************************************************)
+(* The type of constructions *)
+
+type constr =
+  | Rel       of int
+  | Var       of identifier
+  | Meta      of metavariable
+  | Evar      of constr pexistential
+  | Sort      of sorts
+  | Cast      of constr * cast_kind * constr
+  | Prod      of name * constr * constr
+  | Lambda    of name * constr * constr
+  | LetIn     of name * constr * constr * constr
+  | App       of constr * constr array
+  | Const     of constant
+  | Ind       of inductive
+  | Construct of constructor
+  | Case      of case_info * constr * constr * constr array
+  | Fix       of constr pfixpoint
+  | CoFix     of constr pcofixpoint
+
+type existential = constr pexistential
+type rec_declaration = constr prec_declaration
+type fixpoint = constr pfixpoint
+type cofixpoint = constr pcofixpoint
+
+let rec strip_outer_cast c = match c with
+  | Cast (c,_,_) -> strip_outer_cast c
+  | _ -> c
+
+let rec collapse_appl c = match c with
+  | App (f,cl) -> 
+      let rec collapse_rec f cl2 =
+        match (strip_outer_cast f) with
+	| App (g,cl1) -> collapse_rec g (Array.append cl1 cl2)
+	| _ -> App (f,cl2)
+      in
+      collapse_rec f cl
+  | _ -> c
+
+let decompose_app c =
+  match collapse_appl c with
+    | App (f,cl) -> (f, Array.to_list cl)
+    | _ -> (c,[])
+
+
+let applist (f,l) = App (f, Array.of_list l)
+
+
+(****************************************************************************)
+(*              Functions for dealing with constr terms                     *)
+(****************************************************************************)
+
+(*********************)
+(*     Occurring     *)
+(*********************)
+
+let iter_constr_with_binders g f n c = match c with
+  | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
+    | Construct _) -> ()
+  | Cast (c,_,t) -> f n c; f n t
+  | Prod (_,t,c) -> f n t; f (g n) c
+  | Lambda (_,t,c) -> f n t; f (g n) c
+  | LetIn (_,b,t,c) -> f n b; f n t; f (g n) c
+  | App (c,l) -> f n c; Array.iter (f n) l
+  | Evar (_,l) -> Array.iter (f n) l
+  | Case (_,p,c,bl) -> f n p; f n c; Array.iter (f n) bl
+  | Fix (_,(_,tl,bl)) -> 
+      Array.iter (f n) tl;
+      Array.iter (f (iterate g (Array.length tl) n)) bl
+  | CoFix (_,(_,tl,bl)) ->
+      Array.iter (f n) tl;
+      Array.iter (f (iterate g (Array.length tl) n)) bl
+
+exception LocalOccur
+
+(* (closedn n M) raises FreeVar if a variable of height greater than n
+   occurs in M, returns () otherwise *)
+
+let closedn n c = 
+  let rec closed_rec n c = match c with
+    | Rel m -> if m>n then raise LocalOccur
+    | _ -> iter_constr_with_binders succ closed_rec n c
+  in 
+  try closed_rec n c; true with LocalOccur -> false
+
+(* [closed0 M] is true iff [M] is a (deBruijn) closed term *)
+
+let closed0 = closedn 0
+
+(* (noccurn n M) returns true iff (Rel n) does NOT occur in term M  *)
+
+let noccurn n term = 
+  let rec occur_rec n c = match c with
+    | Rel m -> if m = n then raise LocalOccur
+    | _ -> iter_constr_with_binders succ occur_rec n c
+  in 
+  try occur_rec n term; true with LocalOccur -> false
+
+(* (noccur_between n m M) returns true iff (Rel p) does NOT occur in term M 
+  for n <= p < n+m *)
+
+let noccur_between n m term = 
+  let rec occur_rec n c = match c with
+    | Rel(p) -> if n<=p && p<n+m then raise LocalOccur
+    | _        -> iter_constr_with_binders succ occur_rec n c
+  in 
+  try occur_rec n term; true with LocalOccur -> false
+
+(* Checking function for terms containing existential variables.
+ The function [noccur_with_meta] considers the fact that
+ each existential variable (as well as each isevar)
+ in the term appears applied to its local context,
+ which may contain the CoFix variables. These occurrences of CoFix variables
+ are not considered *)
+
+let noccur_with_meta n m term = 
+  let rec occur_rec n c = match c with
+    | Rel p -> if n<=p & p<n+m then raise LocalOccur
+    | App(f,cl) ->
+	(match f with
+           | (Cast (Meta _,_,_)| Meta _) -> ()
+	   | _ -> iter_constr_with_binders succ occur_rec n c)
+    | Evar (_, _) -> ()
+    | _ -> iter_constr_with_binders succ occur_rec n c
+  in
+  try (occur_rec n term; true) with LocalOccur -> false
+
+
+(*********************)
+(*      Lifting      *)
+(*********************)
+
+let map_constr_with_binders g f l c = match c with
+  | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
+    | Construct _) -> c
+  | Cast (c,k,t) -> Cast (f l c, k, f l t)
+  | Prod (na,t,c) -> Prod (na, f l t, f (g l) c)
+  | Lambda (na,t,c) -> Lambda (na, f l t, f (g l) c)
+  | LetIn (na,b,t,c) -> LetIn (na, f l b, f l t, f (g l) c)
+  | App (c,al) -> App (f l c, Array.map (f l) al)
+  | Evar (e,al) -> Evar (e, Array.map (f l) al)
+  | Case (ci,p,c,bl) -> Case (ci, f l p, f l c, Array.map (f l) bl)
+  | Fix (ln,(lna,tl,bl)) ->
+      let l' = iterate g (Array.length tl) l in
+      Fix (ln,(lna,Array.map (f l) tl,Array.map (f l') bl))
+  | CoFix(ln,(lna,tl,bl)) ->
+      let l' = iterate g (Array.length tl) l in
+      CoFix (ln,(lna,Array.map (f l) tl,Array.map (f l') bl))
+
+(* The generic lifting function *)
+let rec exliftn el c = match c with
+  | Rel i -> Rel(reloc_rel i el)
+  | _ -> map_constr_with_binders el_lift exliftn el c
+
+(* 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
+
+(*********************)
+(*   Substituting    *)
+(*********************)
+
+(* (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 c =
+  let lv = Array.length lamv in 
+  if lv = 0 then c
+  else 
+    let rec substrec depth c = match c with
+      | Rel k     ->
+          if k<=depth then c
+          else if k-depth <= lv then lift_substituend depth lamv.(k-depth-1)
+          else Rel (k-lv)
+      | _ -> map_constr_with_binders succ substrec depth c in 
+    substrec n c
+
+let substnl laml n =
+  substn_many (Array.map make_substituend (Array.of_list laml)) n
+let substl laml = substnl laml 0
+let subst1 lam = substl [lam]
+
+
+(***************************************************************************)
+(*     Type of assumptions and contexts                                    *)
+(***************************************************************************)
+
+type named_declaration = identifier * constr option * constr
+type rel_declaration = name * constr option * constr
+
+let map_named_declaration f (id, v, ty) = (id, Option.map f v, f ty)
+let map_rel_declaration = map_named_declaration
+
+let fold_named_declaration f (_, v, ty) a = f ty (Option.fold_right f v a)
+let fold_rel_declaration = fold_named_declaration
+
+
+type named_context = named_declaration list
+let empty_named_context = []
+let fold_named_context f l ~init = List.fold_right f l init
+
+type section_context = named_context
+
+type rel_context = rel_declaration list
+let empty_rel_context = []
+let rel_context_length = List.length
+let rel_context_nhyps hyps =
+  let rec nhyps acc = function
+    | [] -> acc
+    | (_,None,_)::hyps -> nhyps (1+acc) hyps
+    | (_,Some _,_)::hyps -> nhyps acc hyps in
+  nhyps 0 hyps
+let fold_rel_context f l ~init = List.fold_right f l init
+
+let map_context f l =
+  let map_decl (n, body_o, typ as decl) =
+    let body_o' = Option.smartmap f body_o in
+    let typ' = f typ in
+      if body_o' == body_o && typ' == typ then decl else
+	(n, body_o', typ')
+  in
+    list_smartmap map_decl l
+
+let map_rel_context = map_context
+
+let extended_rel_list n hyps =
+  let rec reln l p = function
+    | (_,None,_) :: hyps -> reln (Rel (n+p) :: l) (p+1) hyps
+    | (_,Some _,_) :: hyps -> reln l (p+1) hyps
+    | [] -> l
+  in 
+  reln [] 1 hyps
+
+(* Iterate lambda abstractions *)
+
+(* compose_lam [xn:Tn;..;x1:T1] b = [x1:T1]..[xn:Tn]b *)
+let compose_lam l b =
+  let rec lamrec = function
+    | ([], b)       -> b
+    | ((v,t)::l, b) -> lamrec (l, Lambda (v,t,b))
+  in 
+  lamrec (l,b)
+
+(* 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 c = match c with
+    | Lambda (x,t,c) -> lamdec_rec ((x,t)::l) c
+    | Cast (c,_,_)     -> lamdec_rec l c
+    | _                -> l,c
+  in 
+  lamdec_rec []
+
+(* Decompose lambda abstractions and lets, until finding n
+  abstractions *)
+let decompose_lam_n_assum n =
+  if n < 0 then
+    error "decompose_lam_n_assum: integer parameter must be positive";
+  let rec lamdec_rec l n c = 
+    if n=0 then l,c 
+    else match c with 
+    | Lambda (x,t,c)  -> lamdec_rec ((x,None,t) :: l) (n-1) c
+    | LetIn (x,b,t,c) -> lamdec_rec ((x,Some b,t) :: l) n c
+    | Cast (c,_,_)      -> lamdec_rec l n c
+    | c -> error "decompose_lam_n_assum: not enough abstractions"
+  in 
+  lamdec_rec empty_rel_context n 
+
+(* Iterate products, with or without lets *)
+
+(* Constructs either [(x:t)c] or [[x=b:t]c] *)
+let mkProd_or_LetIn (na,body,t) c =
+  match body with
+    | None -> Prod (na, t, c)
+    | Some b -> LetIn (na, b, t, c)
+
+let it_mkProd_or_LetIn   = List.fold_left (fun c d -> mkProd_or_LetIn d c)
+
+let decompose_prod_assum = 
+  let rec prodec_rec l c =
+    match c with
+    | Prod (x,t,c)    -> prodec_rec ((x,None,t) :: l) c
+    | LetIn (x,b,t,c) -> prodec_rec ((x,Some b,t) :: l) c
+    | Cast (c,_,_)    -> prodec_rec l c
+    | _               -> l,c
+  in 
+  prodec_rec empty_rel_context
+
+let decompose_prod_n_assum n =
+  if n < 0 then
+    error "decompose_prod_n_assum: integer parameter must be positive";
+  let rec prodec_rec l n c = 
+    if n=0 then l,c
+    else match c with 
+    | Prod (x,t,c)    -> prodec_rec ((x,None,t) :: l) (n-1) c
+    | LetIn (x,b,t,c) -> prodec_rec ((x,Some b,t) :: l) (n-1) c
+    | Cast (c,_,_)    -> prodec_rec l n c
+    | c -> error "decompose_prod_n_assum: not enough assumptions"
+  in 
+  prodec_rec empty_rel_context n
+
+
+(***************************)
+(* Other term constructors *)
+(***************************)
+
+type arity = rel_context * sorts
+
+let mkArity (sign,s) = it_mkProd_or_LetIn (Sort s) sign
+
+let destArity = 
+  let rec prodec_rec l c =
+    match c with
+    | Prod (x,t,c)    -> prodec_rec ((x,None,t)::l) c
+    | LetIn (x,b,t,c) -> prodec_rec ((x,Some b,t)::l) c
+    | Cast (c,_,_)    -> prodec_rec l c
+    | Sort s          -> l,s
+    | _               -> anomaly "destArity: not an arity"
+  in 
+  prodec_rec []
+
+let rec isArity c =
+  match c with
+  | Prod (_,_,c)    -> isArity c
+  | LetIn (_,b,_,c) -> isArity (subst1 b c)
+  | Cast (c,_,_)    -> isArity c
+  | Sort _          -> true
+  | _               -> false
+
+(*******************************)
+(*  alpha conversion functions *)                         
+(*******************************)
+
+(* alpha conversion : ignore print names and casts *)
+
+let compare_constr f t1 t2 =
+  match t1, t2 with
+  | Rel n1, Rel n2 -> n1 = n2
+  | Meta m1, Meta m2 -> m1 = m2
+  | Var id1, Var id2 -> id1 = id2
+  | Sort s1, Sort s2 -> s1 = s2
+  | Cast (c1,_,_), _ -> f c1 t2
+  | _, Cast (c2,_,_) -> f t1 c2
+  | Prod (_,t1,c1), Prod (_,t2,c2) -> f t1 t2 & f c1 c2
+  | Lambda (_,t1,c1), Lambda (_,t2,c2) -> f t1 t2 & f c1 c2
+  | LetIn (_,b1,t1,c1), LetIn (_,b2,t2,c2) -> f b1 b2 & f t1 t2 & f c1 c2
+  | App (c1,l1), App (c2,l2) ->
+      if Array.length l1 = Array.length l2 then
+        f c1 c2 & array_for_all2 f l1 l2
+      else
+        let (h1,l1) = decompose_app t1 in        
+        let (h2,l2) = decompose_app t2 in
+        if List.length l1 = List.length l2 then
+          f h1 h2 & List.for_all2 f l1 l2
+        else false
+  | Evar (e1,l1), Evar (e2,l2) -> e1 = e2 & array_for_all2 f l1 l2
+  | Const c1, Const c2 -> c1 = c2
+  | Ind c1, Ind c2 -> c1 = c2
+  | Construct c1, Construct c2 -> c1 = c2
+  | Case (_,p1,c1,bl1), Case (_,p2,c2,bl2) ->
+      f p1 p2 & f c1 c2 & array_for_all2 f bl1 bl2
+  | Fix (ln1,(_,tl1,bl1)), Fix (ln2,(_,tl2,bl2)) ->
+      ln1 = ln2 & array_for_all2 f tl1 tl2 & array_for_all2 f bl1 bl2
+  | CoFix(ln1,(_,tl1,bl1)), CoFix(ln2,(_,tl2,bl2)) ->
+      ln1 = ln2 & array_for_all2 f tl1 tl2 & array_for_all2 f bl1 bl2
+  | _ -> false
+
+let rec eq_constr m n = 
+  (m==n) or
+  compare_constr eq_constr m n
+
+let eq_constr m n = eq_constr m n (* to avoid tracing a recursive fun *)
-- 
cgit v1.2.3