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)]
30 | C.Abst _ -> assert false
34 (*CSC: sbagliato: manca il when *)
36 let counter = ref 0 in
38 (function (name,_,ty,bo) ->
39 let res = Some (C.Name name, (C.Def (C.Fix (!counter,ifl)))) in
44 let counter = ref 0 in
46 (function (name,ty,bo) ->
47 let res = Some (C.Name name,(C.Def (C.CoFix (!counter,ifl)))) in
52 binding@(aux parentid)
57 exception NotImplemented;;
59 (* A subterm is changed into a fresh meta *)
60 let to_sequent id ids_to_terms ids_to_father_ids =
61 let module P = ProofEngine in
62 let term = Hashtbl.find ids_to_terms id in
63 let context = get_context ids_to_terms ids_to_father_ids id in
67 | Some (_,metasenv,_,_) -> metasenv
69 let ty = CicTypeChecker.type_of_aux' metasenv context term in
70 P.perforate context term ty (* P.perforate also sets the goal *)
73 exception FocusOnlyOnMeta;;
75 (* If the current selection is a Meta, that Meta becomes the current goal *)
76 let focus id ids_to_terms ids_to_father_ids =
77 let module P = ProofEngine in
78 let term = Hashtbl.find ids_to_terms id in
79 let context = get_context ids_to_terms ids_to_father_ids id in
83 | Some (_,metasenv,_,_) -> metasenv
85 let ty = CicTypeChecker.type_of_aux' metasenv context term in
87 Cic.Meta (n,_) -> P.goal := Some n
88 | _ -> raise FocusOnlyOnMeta