val context : NCic.context
end
-module NCicBlob(C : NCicContext) : Terms.Blob with type t = NCic.term = struct
+module NCicBlob(C : NCicContext) : Terms.Blob
+with type t = NCic.term and type input = NCic.term = struct
type t = NCic.term
let rec compare x y =
match x,y with
- | NCic.Rel i, NCic.Rel j -> i-j
+ | NCic.Rel i, NCic.Rel j -> j-i
| NCic.Meta (i,_), NCic.Meta (j,_) -> i-j
| NCic.Const r1, NCic.Const r2 -> NReference.compare r1 r2
| NCic.Appl l1, NCic.Appl l2 -> FoUtils.lexicograph compare l1 l2
let pp t =
NCicPp.ppterm ~context:C.context ~metasenv:C.metasenv ~subst:C.subst t;;
+ type input = NCic.term
+
let rec embed = function
| NCic.Meta (i,_) -> Terms.Var i, [i]
| NCic.Appl l ->
NCic.Const r
;;
- let eq_ind =
- let r =
- OCic2NCic.reference_of_oxuri
- (UriManager.uri_of_string
- "cic:/matita/logic/equality/eq_ind.con")
- in
- NCic.Const r
- ;;
-
- let eq_ind_r =
- let r =
- OCic2NCic.reference_of_oxuri
- (UriManager.uri_of_string
- "cic:/matita/logic/equality/eq_elim_r.con")
- in
- NCic.Const r
- ;;
-
- let extract lift vl t =
- let rec pos i = function
- | [] -> raise Not_found
- | j :: tl when j <> i -> 1+ pos i tl
- | _ -> 1
- in
- let vl_len = List.length vl in
- let rec extract = function
- | Terms.Leaf x -> NCicSubstitution.lift (vl_len+lift) x
- | Terms.Var j ->
- (try NCic.Rel (pos j vl) with Not_found -> NCic.Implicit `Term)
- | Terms.Node l -> NCic.Appl (List.map extract l)
- in
- extract t
- ;;
-
- let rec ppfot = function
- | Terms.Leaf _ -> "."
- | Terms.Var i -> "?" ^ string_of_int i
- | Terms.Node l -> "(" ^ String.concat " " (List.map ppfot l) ^ ")"
- ;;
-
- let mk_predicate amount ft p vl =
- let rec aux t p =
- match p with
- | [] -> NCic.Rel 1
- | n::tl ->
- match t with
- | Terms.Leaf _
- | Terms.Var _ ->
- prerr_endline ("term: " ^ ppfot ft);
- prerr_endline ("path: " ^ String.concat ","
- (List.map string_of_int p));
- assert false
- | Terms.Node l ->
- let l =
- HExtlib.list_mapi
- (fun t i ->
- if i = n then aux t tl
- else extract amount (0::vl) t)
- l
- in
- NCic.Appl l
- in
- NCic.Lambda("x", NCic.Implicit `Type, aux ft (List.rev p))
- ;;
-
- let mk_proof (bag : NCic.term Terms.bag) steps =
- let module Subst = FoSubst in
- let position i l =
- let rec aux = function
- | [] -> assert false
- | (j,_) :: tl when i = j -> 1
- | _ :: tl -> 1 + aux tl
- in
- aux l
- in
- let vars_of i l = fst (List.assoc i l) in
- let ty_of i l = snd (List.assoc i l) in
- let close_with_lambdas vl t =
- List.fold_left
- (fun t i ->
- NCic.Lambda ("x"^string_of_int i, NCic.Implicit `Type, t))
- t vl
- in
- let rec aux seen = function
- | [] -> NCic.Rel 1
- | id :: tl ->
-(* prerr_endline ("Let4 : " ^string_of_int id); *)
- let amount = List.length seen in
- let _, lit, vl, proof = Terms.M.find id bag in
- let lit =
- match lit with
- | Terms.Predicate t -> assert false
- | Terms.Equation (l,r,ty,_) ->
- Terms.Node [ Terms.Leaf eqP; ty; l; r]
- in
-(* prerr_endline ("X" ^ ppfot lit); *)
- match proof with
- | Terms.Exact ft ->
- NCic.LetIn ("clause_" ^ string_of_int id, NCic.Implicit `Type,
- close_with_lambdas vl (extract amount vl ft),
- aux ((id,(List.map (fun x -> Terms.Var x) vl,lit))::seen) tl)
- | Terms.Step (_, id1, id2, dir, pos, subst) ->
- let proof_of_id id =
- let vars = vars_of id seen in
- let args = List.map (Subst.apply_subst subst) vars in
- let args = List.map (extract amount vl) args in
- NCic.Appl (NCic.Rel (List.length vl + position id seen) :: args)
- in
- let p_id1 = proof_of_id id1 in
- let p_id2 = proof_of_id id2 in
- let pred =
- let id1_ty = ty_of id1 seen in
- mk_predicate amount (Subst.apply_subst subst id1_ty) pos vl
- in
- let eq_ind = if dir=Terms.Left2Right then eq_ind else eq_ind_r in
- NCic.LetIn ("clause_" ^ string_of_int id, NCic.Implicit `Type,
- close_with_lambdas vl
- (NCic.Appl [ eq_ind ; NCic.Implicit `Type;
- pred; NCic.Implicit `Term; p_id1;
- NCic.Implicit `Term; p_id2 ]),
- aux ((id,(List.map (fun x -> Terms.Var x) vl,lit))::seen) tl)
- in
- aux [] steps
- ;;
-
end