aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/termops.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/termops.ml')
-rw-r--r--pretyping/termops.ml208
1 files changed, 104 insertions, 104 deletions
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 47bc97251..f0a7ce4c8 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -42,7 +42,7 @@ let rec pr_constr c = match kind_of_term c with
| Meta n -> str "Meta(" ++ int n ++ str ")"
| Var id -> pr_id id
| Sort s -> print_sort s
- | Cast (c,_, t) -> hov 1
+ | Cast (c,_, t) -> hov 1
(str"(" ++ pr_constr c ++ cut() ++
str":" ++ pr_constr t ++ str")")
| Prod (Name(id),t,c) -> hov 1
@@ -99,7 +99,7 @@ let pr_var_decl env (id,c,typ) =
let pbody = match c with
| None -> (mt ())
| Some c ->
- (* Force evaluation *)
+ (* Force evaluation *)
let pb = print_constr_env env c in
(str" := " ++ pb ++ cut () ) in
let pt = print_constr_env env typ in
@@ -110,7 +110,7 @@ let pr_rel_decl env (na,c,typ) =
let pbody = match c with
| None -> mt ()
| Some c ->
- (* Force evaluation *)
+ (* Force evaluation *)
let pb = print_constr_env env c in
(str":=" ++ spc () ++ pb ++ spc ()) in
let ptyp = print_constr_env env typ in
@@ -120,39 +120,39 @@ let pr_rel_decl env (na,c,typ) =
let print_named_context env =
hv 0 (fold_named_context
- (fun env d pps ->
+ (fun env d pps ->
pps ++ ws 2 ++ pr_var_decl env d)
env ~init:(mt ()))
-let print_rel_context env =
+let print_rel_context env =
hv 0 (fold_rel_context
(fun env d pps -> pps ++ ws 2 ++ pr_rel_decl env d)
env ~init:(mt ()))
-
+
let print_env env =
let sign_env =
fold_named_context
(fun env d pps ->
let pidt = pr_var_decl env d in
(pps ++ fnl () ++ pidt))
- env ~init:(mt ())
+ env ~init:(mt ())
in
let db_env =
fold_rel_context
(fun env d pps ->
let pnat = pr_rel_decl env d in (pps ++ fnl () ++ pnat))
env ~init:(mt ())
- in
+ in
(sign_env ++ db_env)
-
+
(*let current_module = ref empty_dirpath
let set_module m = current_module := m*)
-let new_univ =
+let new_univ =
let univ_gen = ref 0 in
(fun sp ->
- incr univ_gen;
+ incr univ_gen;
Univ.make_univ (Lib.library_dp(),!univ_gen))
let new_Type () = mkType (new_univ ())
let new_Type_sort () = Type (new_univ ())
@@ -173,7 +173,7 @@ let refresh_universes_gen strict t =
let refresh_universes = refresh_universes_gen false
let refresh_universes_strict = refresh_universes_gen true
-let new_sort_in_family = function
+let new_sort_in_family = function
| InProp -> prop_sort
| InSet -> set_sort
| InType -> Type (new_univ ())
@@ -183,10 +183,10 @@ let new_sort_in_family = function
(* [Rel (n+m);...;Rel(n+1)] *)
let rel_vect n m = Array.init m (fun i -> mkRel(n+m-i))
-let rel_list n m =
- let rec reln l p =
+let rel_list n m =
+ let rec reln l p =
if p>m then l else reln (mkRel(n+p)::l) (p+1)
- in
+ in
reln [] 1
(* Same as [rel_list] but takes a context as argument and skips let-ins *)
@@ -195,7 +195,7 @@ let extended_rel_list n hyps =
| (_,None,_) :: hyps -> reln (mkRel (n+p) :: l) (p+1) hyps
| (_,Some _,_) :: hyps -> reln l (p+1) hyps
| [] -> l
- in
+ in
reln [] 1 hyps
let extended_rel_vect n hyps = Array.of_list (extended_rel_list n hyps)
@@ -218,12 +218,12 @@ let push_named_rec_types (lna,typarray,_) env =
Array.fold_left
(fun e assum -> push_named assum e) env ctxt
-let rec lookup_rel_id id sign =
+let rec lookup_rel_id id sign =
let rec lookrec = function
| (n, (Anonymous,_,_)::l) -> lookrec (n+1,l)
| (n, (Name id',_,t)::l) -> if id' = id then (n,t) else lookrec (n+1,l)
| (_, []) -> raise Not_found
- in
+ in
lookrec (1,sign)
(* Constructs either [forall x:t, c] or [let x:=b:t in c] *)
@@ -241,7 +241,7 @@ let mkProd_wo_LetIn (na,body,t) c =
let it_mkProd ~init = List.fold_left (fun c (n,t) -> mkProd (n, t, c)) init
let it_mkLambda ~init = List.fold_left (fun c (n,t) -> mkLambda (n, t, c)) init
-let it_named_context_quantifier f ~init =
+let it_named_context_quantifier f ~init =
List.fold_left (fun c d -> f d c) init
let it_mkProd_or_LetIn = it_named_context_quantifier mkProd_or_LetIn
@@ -255,12 +255,12 @@ let it_mkNamedLambda_or_LetIn = it_named_context_quantifier mkNamedLambda_or_Let
(* strips head casts and flattens head applications *)
let rec strip_head_cast c = match kind_of_term c with
- | App (f,cl) ->
+ | App (f,cl) ->
let rec collapse_rec f cl2 = match kind_of_term f with
| App (g,cl1) -> collapse_rec g (Array.append cl1 cl2)
| Cast (c,_,_) -> collapse_rec c cl2
| _ -> if Array.length cl2 = 0 then f else mkApp (f,cl2)
- in
+ in
collapse_rec f cl
| Cast (c,_,_) -> strip_head_cast c
| _ -> c
@@ -348,7 +348,7 @@ let map_constr_with_binders_left_to_right g f l c = match kind_of_term c with
let map_constr_with_full_binders g f l cstr = match kind_of_term cstr with
| (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _
| Construct _) -> cstr
- | Cast (c,k, t) ->
+ | Cast (c,k, t) ->
let c' = f l c in
let t' = f l t in
if c==c' && t==t' then cstr else mkCast (c', k, t')
@@ -412,7 +412,7 @@ let fold_constr_with_binders g f n acc c = match kind_of_term c with
| App (c,l) -> Array.fold_left (f n) (f n acc c) l
| Evar (_,l) -> Array.fold_left (f n) acc l
| Case (_,p,c,bl) -> Array.fold_left (f n) (f n (f n acc p) c) bl
- | Fix (_,(lna,tl,bl)) ->
+ | Fix (_,(lna,tl,bl)) ->
let n' = iterate g (Array.length tl) n in
let fd = array_map2 (fun t b -> (t,b)) tl bl in
Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd
@@ -436,7 +436,7 @@ let iter_constr_with_full_binders g f l c = match kind_of_term c with
| App (c,args) -> f l c; Array.iter (f l) args
| Evar (_,args) -> Array.iter (f l) args
| Case (_,p,c,bl) -> f l p; f l c; Array.iter (f l) bl
- | Fix (_,(lna,tl,bl)) ->
+ | Fix (_,(lna,tl,bl)) ->
let l' = array_fold_left2 (fun l na t -> g (na,None,t) l) l lna tl in
Array.iter (f l) tl;
Array.iter (f l') bl
@@ -446,7 +446,7 @@ let iter_constr_with_full_binders g f l c = match kind_of_term c with
Array.iter (f l') bl
(***************************)
-(* occurs check functions *)
+(* occurs check functions *)
(***************************)
exception Occur
@@ -457,42 +457,42 @@ let occur_meta c =
| _ -> iter_constr occrec c
in try occrec c; false with Occur -> true
-let occur_existential c =
+let occur_existential c =
let rec occrec c = match kind_of_term c with
| Evar _ -> raise Occur
| _ -> iter_constr occrec c
in try occrec c; false with Occur -> true
-let occur_meta_or_existential c =
+let occur_meta_or_existential c =
let rec occrec c = match kind_of_term c with
| Evar _ -> raise Occur
| Meta _ -> raise Occur
| _ -> iter_constr occrec c
in try occrec c; false with Occur -> true
-let occur_const s c =
+let occur_const s c =
let rec occur_rec c = match kind_of_term c with
| Const sp when sp=s -> raise Occur
| _ -> iter_constr occur_rec c
- in
+ in
try occur_rec c; false with Occur -> true
-let occur_evar n c =
+let occur_evar n c =
let rec occur_rec c = match kind_of_term c with
| Evar (sp,_) when sp=n -> raise Occur
| _ -> iter_constr occur_rec c
- in
+ in
try occur_rec c; false with Occur -> true
let occur_in_global env id constr =
let vars = vars_of_global env constr in
if List.mem id vars then raise Occur
-let occur_var env s c =
+let occur_var env s c =
let rec occur_rec c =
occur_in_global env s c;
iter_constr occur_rec c
- in
+ in
try occur_rec c; false with Occur -> true
let occur_var_in_decl env hyp (_,c,typ) =
@@ -504,17 +504,17 @@ let occur_var_in_decl env hyp (_,c,typ) =
(* returns the list of free debruijn indices in a term *)
-let free_rels m =
+let free_rels m =
let rec frec depth acc c = match kind_of_term c with
| Rel n -> if n >= depth then Intset.add (n-depth+1) acc else acc
| _ -> fold_constr_with_binders succ frec depth acc c
- in
+ in
frec 1 Intset.empty m
(* collects all metavar occurences, in left-to-right order, preserving
* repetitions and all. *)
-let collect_metas c =
+let collect_metas c =
let rec collrec acc c =
match kind_of_term c with
| Meta mv -> list_add_set mv acc
@@ -534,12 +534,12 @@ let dependent_main noevar m t =
| App (fm,lm), App (ft,lt) when Array.length lm < Array.length lt ->
deprec m (mkApp (ft,Array.sub lt 0 (Array.length lm)));
Array.iter (deprec m)
- (Array.sub lt
+ (Array.sub lt
(Array.length lm) ((Array.length lt) - (Array.length lm)))
| _, Cast (c,_,_) when noevar & isMeta c -> ()
| _, Evar _ when noevar -> ()
| _ -> iter_constr_with_binders (lift 1) deprec m t
- in
+ in
try deprec m t; false with Occur -> true
let dependent = dependent_main false
@@ -551,21 +551,21 @@ let occur_term = dependent
let pop t = lift (-1) t
(***************************)
-(* bindings functions *)
+(* bindings functions *)
(***************************)
-type meta_type_map = (metavariable * types) list
+type meta_type_map = (metavariable * types) list
-type meta_value_map = (metavariable * constr) list
+type meta_value_map = (metavariable * constr) list
-let rec subst_meta bl c =
+let rec subst_meta bl c =
match kind_of_term c with
| Meta i -> (try List.assoc i bl with Not_found -> c)
| _ -> map_constr (subst_meta bl) c
(* First utilities for avoiding telescope computation for subst_term *)
-let prefix_application eq_fun (k,c) (t : constr) =
+let prefix_application eq_fun (k,c) (t : constr) =
let c' = collapse_appl c and t' = collapse_appl t in
match kind_of_term c', kind_of_term t' with
| App (f1,cl1), App (f2,cl2) ->
@@ -574,11 +574,11 @@ let prefix_application eq_fun (k,c) (t : constr) =
if l1 <= l2
&& eq_fun c' (mkApp (f2, Array.sub cl2 0 l1)) then
Some (mkApp (mkRel k, Array.sub cl2 l1 (l2 - l1)))
- else
+ else
None
| _ -> None
-let my_prefix_application eq_fun (k,c) (by_c : constr) (t : constr) =
+let my_prefix_application eq_fun (k,c) (by_c : constr) (t : constr) =
let c' = collapse_appl c and t' = collapse_appl t in
match kind_of_term c', kind_of_term t' with
| App (f1,cl1), App (f2,cl2) ->
@@ -587,7 +587,7 @@ let my_prefix_application eq_fun (k,c) (by_c : constr) (t : constr) =
if l1 <= l2
&& eq_fun c' (mkApp (f2, Array.sub cl2 0 l1)) then
Some (mkApp ((lift k by_c), Array.sub cl2 l1 (l2 - l1)))
- else
+ else
None
| _ -> None
@@ -596,7 +596,7 @@ let my_prefix_application eq_fun (k,c) (by_c : constr) (t : constr) =
term [c] in a term [t] *)
(*i Bizarre : si on cherche un sous terme clos, pourquoi le lifter ? i*)
-let subst_term_gen eq_fun c t =
+let subst_term_gen eq_fun c t =
let rec substrec (k,c as kc) t =
match prefix_application eq_fun kc t with
| Some x -> x
@@ -604,7 +604,7 @@ let subst_term_gen eq_fun c t =
if eq_fun c t then mkRel k
else
map_constr_with_binders (fun (k,c) -> (k+1,lift 1 c)) substrec kc t
- in
+ in
substrec (1,c) t
(* Recognizing occurrences of a given (closed) subterm in a term :
@@ -612,7 +612,7 @@ let subst_term_gen eq_fun c t =
term [c1] in a term [t] *)
(*i Meme remarque : a priori [c] n'est pas forcement clos i*)
-let replace_term_gen eq_fun c by_c in_t =
+let replace_term_gen eq_fun c by_c in_t =
let rec substrec (k,c as kc) t =
match my_prefix_application eq_fun kc by_c t with
| Some x -> x
@@ -620,7 +620,7 @@ let replace_term_gen eq_fun c by_c in_t =
(if eq_fun c t then (lift k by_c) else
map_constr_with_binders (fun (k,c) -> (k+1,lift 1 c))
substrec kc t)
- in
+ in
substrec (0,c) in_t
let subst_term = subst_term_gen eq_constr
@@ -639,7 +639,7 @@ let no_occurrences_in_set = (true,[])
let error_invalid_occurrence l =
let l = list_uniquize (List.sort Pervasives.compare l) in
errorlabstrm ""
- (str ("Invalid occurrence " ^ plural (List.length l) "number" ^": ") ++
+ (str ("Invalid occurrence " ^ plural (List.length l) "number" ^": ") ++
prlist_with_sep spc int l ++ str ".")
let subst_term_occ_gen (nowhere_except_in,locs) occ c t =
@@ -650,10 +650,10 @@ let subst_term_occ_gen (nowhere_except_in,locs) occ c t =
if nowhere_except_in & !pos > maxocc then t
else
if eq_constr c t then
- let r =
+ let r =
if nowhere_except_in then
if List.mem !pos locs then (mkRel k) else t
- else
+ else
if List.mem !pos locs then t else (mkRel k)
in incr pos; r
else
@@ -664,9 +664,9 @@ let subst_term_occ_gen (nowhere_except_in,locs) occ c t =
let t' = substrec (1,c) t in
(!pos, t')
-let subst_term_occ (nowhere_except_in,locs as plocs) c t =
+let subst_term_occ (nowhere_except_in,locs as plocs) c t =
if locs = [] then if nowhere_except_in then t else subst_term c t
- else
+ else
let (nbocc,t') = subst_term_occ_gen plocs 1 c t in
let rest = List.filter (fun o -> o >= nbocc) locs in
if rest <> [] then error_invalid_occurrence rest;
@@ -687,7 +687,7 @@ let subst_term_occ_decl ((nowhere_except_in,locs as plocs),hloc) c (id,bodyopt,t
if locs = [] then
if nowhere_except_in then d
else (id,Some (subst_term c body),subst_term c typ)
- else
+ else
let (nbocc,body') = subst_term_occ_gen plocs 1 c body in
let (nbocc',t') = subst_term_occ_gen plocs nbocc c typ in
let rest = List.filter (fun o -> o >= nbocc') locs in
@@ -700,7 +700,7 @@ let lowercase_first_char id =
lowercase_first_char_utf8 (string_of_id id)
let vars_of_env env =
- let s =
+ let s =
Sign.fold_named_context (fun (id,_,_) s -> Idset.add id s)
(named_context env) ~init:Idset.empty in
Sign.fold_rel_context
@@ -717,7 +717,7 @@ let sort_hdchar = function
| Prop(_) -> "P"
| Type(_) -> "T"
-let hdchar env c =
+let hdchar env c =
let rec hdrec k c =
match kind_of_term c with
| Prod (_,_,c) -> hdrec (k+1) c
@@ -728,9 +728,9 @@ let hdchar env c =
| Const kn ->
lowercase_first_char (id_of_label (con_label kn))
| Ind ((kn,i) as x) ->
- if i=0 then
+ if i=0 then
lowercase_first_char (id_of_label (label kn))
- else
+ else
lowercase_first_char (basename_of_global (IndRef x))
| Construct ((sp,i) as x) ->
lowercase_first_char (basename_of_global (ConstructRef x))
@@ -743,22 +743,22 @@ let hdchar env c =
| (Name id,_,_) -> lowercase_first_char id
| (Anonymous,_,t) -> hdrec 0 (lift (n-k) t)
with Not_found -> "y")
- | Fix ((_,i),(lna,_,_)) ->
+ | Fix ((_,i),(lna,_,_)) ->
let id = match lna.(i) with Name id -> id | _ -> assert false in
lowercase_first_char id
- | CoFix (i,(lna,_,_)) ->
+ | CoFix (i,(lna,_,_)) ->
let id = match lna.(i) with Name id -> id | _ -> assert false in
lowercase_first_char id
| Meta _|Evar _|Case (_, _, _, _) -> "y"
- in
+ in
hdrec 0 c
let id_of_name_using_hdchar env a = function
- | Anonymous -> id_of_string (hdchar env a)
+ | Anonymous -> id_of_string (hdchar env a)
| Name id -> id
let named_hd env a = function
- | Anonymous -> Name (id_of_string (hdchar env a))
+ | Anonymous -> Name (id_of_string (hdchar env a))
| x -> x
let mkProd_name env (n,a,b) = mkProd (named_hd env a n, a, b)
@@ -778,11 +778,11 @@ let name_assumption env (na,c,t) =
let name_context env hyps =
snd
(List.fold_left
- (fun (env,hyps) d ->
+ (fun (env,hyps) d ->
let d' = name_assumption env d in (push_rel d' env, d' :: hyps))
(env,[]) (List.rev hyps))
-let mkProd_or_LetIn_name env b d = mkProd_or_LetIn (name_assumption env d) b
+let mkProd_or_LetIn_name env b d = mkProd_or_LetIn (name_assumption env d) b
let mkLambda_or_LetIn_name env b d = mkLambda_or_LetIn (name_assumption env d)b
let it_mkProd_or_LetIn_name env b hyps =
@@ -798,12 +798,12 @@ let add_name n nl = n::nl
let lookup_name_of_rel p names =
try List.nth names (p-1)
with Invalid_argument _ | Failure _ -> raise Not_found
-let rec lookup_rel_of_name id names =
+let rec lookup_rel_of_name id names =
let rec lookrec n = function
| Anonymous :: l -> lookrec (n+1) l
| (Name id') :: l -> if id' = id then n else lookrec (n+1) l
| [] -> raise Not_found
- in
+ in
lookrec 1 names
let empty_names_context = []
@@ -815,7 +815,7 @@ let ids_of_rel_context sign =
let ids_of_named_context sign =
Sign.fold_named_context (fun (id,_,_) idl -> id::idl) sign ~init:[]
-let ids_of_context env =
+let ids_of_context env =
(ids_of_rel_context (rel_context env))
@ (ids_of_named_context (named_context env))
@@ -838,42 +838,42 @@ let is_imported_ref = function
let (mp,_,_) = repr_con kn in is_imported_modpath mp
let is_global id =
- try
+ try
let ref = locate (qualid_of_ident id) in
not (is_imported_ref ref)
- with Not_found ->
+ with Not_found ->
false
let is_constructor id =
- try
- match locate (qualid_of_ident id) with
+ try
+ match locate (qualid_of_ident id) with
| ConstructRef _ as ref -> not (is_imported_ref ref)
| _ -> false
- with Not_found ->
+ with Not_found ->
false
let is_section_variable id =
try let _ = Global.lookup_named id in true
with Not_found -> false
-let next_global_ident_from allow_secvar id avoid =
+let next_global_ident_from allow_secvar id avoid =
let rec next_rec id =
let id = next_ident_away_from id avoid in
if (allow_secvar && is_section_variable id) || not (is_global id) then
id
- else
+ else
next_rec (lift_ident id)
- in
+ in
next_rec id
let next_global_ident_away allow_secvar id avoid =
let id = next_ident_away id avoid in
if (allow_secvar && is_section_variable id) || not (is_global id) then
id
- else
+ else
next_global_ident_from allow_secvar (lift_ident id) avoid
-let isGlobalRef c =
+let isGlobalRef c =
match kind_of_term c with
| Const _ | Ind _ | Construct _ | Var _ -> true
| _ -> false
@@ -884,23 +884,23 @@ let has_polymorphic_type c =
| _ -> false
(* nouvelle version de renommage des variables (DEC 98) *)
-(* This is the algorithm to display distinct bound variables
+(* This is the algorithm to display distinct bound variables
- Règle 1 : un nom non anonyme, même non affiché, contribue à la liste
- des noms à éviter
+ des noms à éviter
- Règle 2 : c'est la dépendance qui décide si on affiche ou pas
- Exemple :
+ Exemple :
si bool_ind = (P:bool->Prop)(f:(P true))(f:(P false))(b:bool)(P b), alors
il est affiché (P:bool->Prop)(P true)->(P false)->(b:bool)(P b)
- mais f et f0 contribue à la liste des variables à éviter (en supposant
+ mais f et f0 contribue à la liste des variables à éviter (en supposant
que les noms f et f0 ne sont pas déjà pris)
Intérêt : noms homogènes dans un but avant et après Intro
*)
type used_idents = identifier list
-let occur_rel p env id =
+let occur_rel p env id =
try lookup_name_of_rel p env = Name id
with Not_found -> false (* Unbound indice : may happen in debug *)
@@ -916,7 +916,7 @@ let occur_id nenv id0 c =
raise Occur
| Rel p when p>n & occur_rel (p-n) nenv id0 -> raise Occur
| _ -> iter_constr_with_binders succ occur n c
- in
+ in
try occur 1 c; false
with Occur -> true
| Not_found -> false (* Case when a global is not in the env *)
@@ -925,7 +925,7 @@ type avoid_flags = bool option
let next_name_not_occuring avoid_flags name l env_names t =
let rec next id =
- if List.mem id l or occur_id env_names id t or
+ if List.mem id l or occur_id env_names id t or
(* Further restrictions ? *)
match avoid_flags with None -> false | Some not_only_cstr ->
(if not_only_cstr then
@@ -936,10 +936,10 @@ let next_name_not_occuring avoid_flags name l env_names t =
is_constructor id)
then next (lift_ident id)
else id
- in
+ in
match name with
| Name id -> next id
- | Anonymous ->
+ | Anonymous ->
(* Normally, an anonymous name is not dependent and will not be *)
(* taken into account by the function concrete_name; just in case *)
(* invent a valid name *)
@@ -953,10 +953,10 @@ let base_sort_cmp pb s0 s1 =
| _ -> false
(* eq_constr extended with universe erasure *)
-let compare_constr_univ f cv_pb t1 t2 =
+let compare_constr_univ f cv_pb t1 t2 =
match kind_of_term t1, kind_of_term t2 with
Sort s1, Sort s2 -> base_sort_cmp cv_pb s1 s2
- | Prod (_,t1,c1), Prod (_,t2,c2) ->
+ | Prod (_,t1,c1), Prod (_,t2,c2) ->
f Reduction.CONV t1 t2 & f cv_pb c1 c2
| _ -> compare_constr (f Reduction.CONV) t1 t2
@@ -967,7 +967,7 @@ let eq_constr = constr_cmp Reduction.CONV
(* App(c,[t1,...tn]) -> ([c,t1,...,tn-1],tn)
App(c,[||]) -> ([],c) *)
let split_app c = match kind_of_term c with
- App(c,l) ->
+ App(c,l) ->
let len = Array.length l in
if len=0 then ([],c) else
let last = Array.get l (len-1) in
@@ -983,16 +983,16 @@ exception CannotFilter
let filtering env cv_pb c1 c2 =
let evm = ref Intmap.empty in
- let define cv_pb e1 ev c1 =
+ let define cv_pb e1 ev c1 =
try let (e2,c2) = Intmap.find ev !evm in
let shift = List.length e1 - List.length e2 in
if constr_cmp cv_pb c1 (lift shift c2) then () else raise CannotFilter
- with Not_found ->
+ with Not_found ->
evm := Intmap.add ev (e1,c1) !evm
in
let rec aux env cv_pb c1 c2 =
match kind_of_term c1, kind_of_term c2 with
- | App _, App _ ->
+ | App _, App _ ->
let ((p1,l1),(p2,l2)) = (split_app c1),(split_app c2) in
aux env cv_pb l1 l2; if p1=[] & p2=[] then () else
aux env cv_pb (applist (hdtl p1)) (applist (hdtl p2))
@@ -1001,15 +1001,15 @@ let filtering env cv_pb c1 c2 =
aux ((n,None,t1)::env) cv_pb c1 c2
| _, Evar (ev,_) -> define cv_pb env ev c1
| Evar (ev,_), _ -> define cv_pb env ev c2
- | _ ->
- if compare_constr_univ
- (fun pb c1 c2 -> aux env pb c1 c2; true) cv_pb c1 c2 then ()
+ | _ ->
+ if compare_constr_univ
+ (fun pb c1 c2 -> aux env pb c1 c2; true) cv_pb c1 c2 then ()
else raise CannotFilter
(* TODO: le reste des binders *)
in
aux env cv_pb c1 c2; !evm
-let decompose_prod_letin : constr -> int * rel_context * constr =
+let decompose_prod_letin : constr -> int * rel_context * constr =
let rec prodec_rec i l c = match kind_of_term c with
| Prod (n,t,c) -> prodec_rec (succ i) ((n,None,t)::l) c
| LetIn (n,d,t,c) -> prodec_rec (succ i) ((n,Some d,t)::l) c
@@ -1023,7 +1023,7 @@ let align_prod_letin c a : rel_context * constr =
if not (la >= lc) then invalid_arg "align_prod_letin";
let (l1,l2) = Util.list_chop lc l in
l2,it_mkProd_or_LetIn a l1
-
+
(* 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 *)
@@ -1033,7 +1033,7 @@ let rec eta_reduce_head c =
| Lambda (_,c1,c') ->
(match kind_of_term (eta_reduce_head c') with
| App (f,cl) ->
- let lastn = (Array.length cl) - 1 in
+ let lastn = (Array.length cl) - 1 in
if lastn < 1 then anomaly "application without arguments"
else
(match kind_of_term cl.(lastn) with
@@ -1107,7 +1107,7 @@ let smash_rel_context sign =
let adjust_subst_to_rel_context sign l =
let rec aux subst sign l =
- match sign, l with
+ match sign, l with
| (_,None,_)::sign', a::args' -> aux (a::subst) sign' args'
| (_,Some c,_)::sign', args' ->
aux (substl (List.rev subst) c :: subst) sign' args'
@@ -1125,7 +1125,7 @@ let rec mem_named_context id = function
let make_all_name_different env =
let avoid = ref (ids_of_named_context (named_context env)) in
process_rel_context
- (fun (na,c,t) newenv ->
+ (fun (na,c,t) newenv ->
let id = next_name_away na !avoid in
avoid := id::!avoid;
push_rel (Name id,c,t) newenv)
@@ -1195,7 +1195,7 @@ let on_judgment f j = { uj_val = f j.uj_val; uj_type = f j.uj_type }
let on_judgment_value f j = { j with uj_val = f j.uj_val }
let on_judgment_type f j = { j with uj_type = f j.uj_type }
-(* Cut a context ctx in 2 parts (ctx1,ctx2) with ctx1 containing k
+(* Cut a context ctx in 2 parts (ctx1,ctx2) with ctx1 containing k
variables *)
let context_chop k ctx =
let rec chop_aux acc = function
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-11 13:46:40 +0000