(* $Id: terms.mli 9822 2009-06-03 15:37:06Z tassi $ *)
-module type NCicContext =
+module type NCicContext =
sig
val metasenv : NCic.metasenv
val subst : NCic.substitution
let pp t =
NCicPp.ppterm ~context:C.context ~metasenv:C.metasenv ~subst:C.subst t;;
+ let rec embed = function
+ | NCic.Meta (i,_) -> Terms.Var i, [i]
+ | NCic.Appl l ->
+ let rec aux acc l = function
+ |[] -> acc@l
+ |hd::tl -> if List.mem hd l then aux acc l tl else aux (hd::acc) l tl
+ in
+ let res,vars = List.fold_left
+ (fun (r,v) t -> let r1,v1 = embed t in (r1::r),aux [] v v1) ([],[]) l
+ in (Terms.Node (List.rev res)), vars
+ | t -> Terms.Leaf t, []
+ ;;
+
+ let embed t = fst (embed t) ;;
+
+ let saturate t ty =
+ let sty, _, args =
+ NCicMetaSubst.saturate ~delta:max_int C.metasenv C.subst C.context
+ ty 0
+ in
+ let proof =
+ if args = [] then Terms.Leaf t
+ else Terms.Node (Terms.Leaf t :: List.map embed args)
+ in
+ let sty = embed sty in
+ proof, sty
+ ;;
+
+ let eqP =
+ let r =
+ OCic2NCic.reference_of_oxuri
+ (UriManager.uri_of_string
+ "cic:/matita/logic/equality/eq.ind#xpointer(1/1)")
+ in
+ NCic.Const r
+ ;;
+
+
end