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 =
10 match get_parent id ids_to_terms ids_to_father_ids with
12 | Some (parentid,parent) ->
13 let term = Hashtbl.find ids_to_terms id in
22 | C.Prod (n,s,t) when t == term -> [Some (n,C.Decl s)]
24 | C.Lambda (n,s,t) when t == term -> [Some (n,C.Decl s)]
26 | C.LetIn (n,s,t) when t == term -> [Some (n,C.Def s)]
33 (*CSC: sbagliato: manca il when *)
35 let counter = ref 0 in
37 (function (name,_,ty,bo) ->
38 let res = Some (C.Name name, (C.Def (C.Fix (!counter,ifl)))) in
43 let counter = ref 0 in
45 (function (name,ty,bo) ->
46 let res = Some (C.Name name,(C.Def (C.CoFix (!counter,ifl)))) in
51 binding@(aux parentid)
56 exception NotImplemented;;
58 (* A subterm is changed into a fresh meta *)
59 let to_sequent id ids_to_terms ids_to_father_ids =
60 let module P = ProofEngine in
61 let term = Hashtbl.find ids_to_terms id in
62 let context = get_context ids_to_terms ids_to_father_ids id in
66 | Some (_,metasenv,_,_) -> metasenv
68 let ty = CicTypeChecker.type_of_aux' metasenv context term in
69 P.perforate context term ty (* P.perforate also sets the goal *)
72 exception FocusOnlyOnMeta;;
74 (* If the current selection is a Meta, that Meta becomes the current goal *)
75 let focus id ids_to_terms ids_to_father_ids =
76 let module P = ProofEngine in
77 let term = Hashtbl.find ids_to_terms id in
78 let context = get_context ids_to_terms ids_to_father_ids id in
82 | Some (_,metasenv,_,_) -> metasenv
84 let ty = CicTypeChecker.type_of_aux' metasenv context term in
86 Cic.Meta (n,_) -> P.goal := Some n
87 | _ -> raise FocusOnlyOnMeta