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
66 let type_checker_env_of_context =
69 P.Declaration,_,t -> t
70 | P.Definition,_,_ -> raise NotImplemented
76 | Some (_,metasenv,_,_) -> metasenv
79 CicTypeChecker.type_of_aux' metasenv type_checker_env_of_context term
81 let (meta,perforated) =
82 (* If the selected term is already a meta, we return it. *)
83 (* Otherwise, we are trying to refine a non-meta term... *)
85 Cic.Meta n -> P.goal := Some (n,(context,ty)) ; n,false
86 | _ -> P.perforate context term ty,true (* P.perforate also sets the goal *)