| C.Rel _ as t -> a,t
| C.Appl [] | C.Appl [_] -> assert false
| C.Appl l as orig ->
+ let fire_beta, upto =
+ match l with C.Meta _ :: _ -> true, List.length l - 1 | _ -> false, 0
+ in
let a,l1 =
(* sharing fold? *)
List.fold_right
(fun t (a,l) -> let a,t = f k a t in a, t :: l)
l (a,[])
in
- a, if l1 == l then orig else (match l1 with
- | C.Appl l :: tl -> C.Appl (l@tl)
- | _ -> C.Appl l1)
+ a, if l1 == l then orig else
+ let t =
+ match l1 with
+ | C.Appl l :: tl -> C.Appl (l@tl)
+ | _ -> C.Appl l1
+ in
+ if fire_beta then NCicReduction.head_beta_reduce ~upto t
+ else t
| C.Prod (n,s,t) as orig ->
let a,s1 = f k a s in let a,t1 = f (g (n,C.Decl s) k) a t in
a, if t1 == t && s1 == s then orig else C.Prod (n,s1,t1)
HExtlib.list_uniq (List.sort Pervasives.compare (aux context [] term))
;;
+module NCicHash =
+ Hashtbl.Make
+ (struct
+ type t = C.term
+ let equal = (==)
+ let hash = Hashtbl.hash_param 100 1000
+ end)
+;;
+
+let mk_appl he args =
+ if args = [] then he else
+ match he with
+ | NCic.Appl l -> NCic.Appl (l@args)
+ | _ -> NCic.Appl (he::args)
+;;
+
+let map_obj_kind f =
+ function
+ NCic.Constant (relev,name,bo,ty,attrs) ->
+ NCic.Constant (relev,name,HExtlib.map_option f bo, f ty,attrs)
+ | NCic.Fixpoint (ind,fl,attrs) ->
+ let fl =
+ List.map
+ (function (relevance,name,recno,ty,bo) -> relevance,name,recno,f ty,f bo)
+ fl
+ in
+ NCic.Fixpoint (ind,fl,attrs)
+ | NCic.Inductive (is_ind,lno,itl,attrs) ->
+ let itl =
+ List.map
+ (fun (relevance,name,ty,cl) ->
+ let cl =
+ List.map (fun (relevance, name, ty) ->
+ relevance, name, f ty)
+ cl
+ in
+ relevance, name, f ty, cl)
+ itl
+ in
+ NCic.Inductive (is_ind,lno,itl,attrs)
+;;
+
+let apply_subst subst t =
+ let rec apply_subst subst () =
+ function
+ NCic.Meta (i,lc) ->
+ (try
+ let _,_,t,_ = NCicUtils.lookup_subst i subst in
+ let t = NCicSubstitution.subst_meta lc t in
+ apply_subst subst () t
+ with
+ Not_found ->
+ match lc with
+ _,NCic.Irl _ -> NCic.Meta (i,lc)
+ | n,NCic.Ctx l ->
+ NCic.Meta
+ (i,(0,NCic.Ctx
+ (List.map (fun t ->
+ apply_subst subst () (NCicSubstitution.lift n t)) l))))
+ | t -> NCicUtils.map (fun _ () -> ()) () (apply_subst subst) t
+ in
+ apply_subst subst () t
+;;
+