1 let get_parent id ids_to_terms ids_to_father_ids =
2 match Hashtbl.find ids_to_father_ids id with
4 | Some id -> Some (id, Hashtbl.find ids_to_terms id)
7 let get_context ids_to_terms ids_to_father_ids =
8 let module P = ProofEngine in
11 match get_parent id ids_to_terms ids_to_father_ids with
13 | Some (parentid,parent) ->
14 let term = Hashtbl.find ids_to_terms id in
23 | C.Prod (n,s,t) when t == term -> [P.Declaration (n,s)]
25 | C.Lambda (n,s,t) when t == term -> [P.Declaration (n,s)]
27 | C.LetIn (n,s,t) when t == term -> [P.Definition (n,s)]
31 | C.Abst _ -> assert false
35 (*CSC: sbagliato: manca il when *)
37 let counter = ref 0 in
39 (function (name,_,ty,bo) ->
40 let res = (P.Definition (C.Name name, C.Fix (!counter,ifl))) in
45 let counter = ref 0 in
47 (function (name,ty,bo) ->
48 let res = (P.Definition (C.Name name, C.CoFix (!counter,ifl))) in
53 binding@(aux parentid)
58 exception NotImplemented;;
60 (* It returns true iff the proof has been perforated, i.e. if a subterm *)
61 (* has been changed into a meta. *)
62 let to_sequent id ids_to_terms ids_to_father_ids =
63 let module P = ProofEngine in
64 let term = Hashtbl.find ids_to_terms id in
65 let context = get_context ids_to_terms ids_to_father_ids id in
69 | Some (_,metasenv,_,_) -> metasenv
72 CicTypeChecker.type_of_aux' metasenv
73 (P.cic_context_of_named_context context) term
75 let (meta,perforated) =
76 (* If the selected term is already a meta, we return it. *)
77 (* Otherwise, we are trying to refine a non-meta term... *)
79 Cic.Meta n -> P.goal := Some (n,(context,ty)) ; n,false
80 | _ -> P.perforate context term ty,true (* P.perforate also sets the goal *)