helm/gTopLevel/logicalOperations.ml

   1 let get_parent id ids_to_terms ids_to_father_ids =
   2  match Hashtbl.find ids_to_father_ids id with
   3     None -> None
   4   | Some id -> Some (id, Hashtbl.find ids_to_terms id)
   5 ;;
   6
   7 let get_context ids_to_terms ids_to_father_ids =
   8  let module C = Cic in
   9   let rec aux id =
  10    match get_parent id ids_to_terms ids_to_father_ids with
  11       None -> []
  12     | Some (parentid,parent) ->
  13        let term = Hashtbl.find ids_to_terms id in
  14        let binding =
  15         match parent with
  16            C.Rel _
  17          | C.Var _
  18          | C.Meta _
  19          | C.Sort _
  20          | C.Implicit
  21          | C.Cast _ -> []
  22          | C.Prod (n,s,t) when t == term -> [Some (n,C.Decl s)]
  23          | C.Prod _ -> []
  24          | C.Lambda (n,s,t) when t == term -> [Some (n,C.Decl s)]
  25          | C.Lambda _ -> []
  26          | C.LetIn (n,s,t) when t == term -> [Some (n,C.Def s)]
  27          | C.LetIn _ -> []
  28          | C.Appl _
  29          | C.Const _ -> []
  30          | C.Abst _ -> assert false
  31          | C.MutInd _
  32          | C.MutConstruct _
  33          | C.MutCase _ -> []
  34 (*CSC: sbagliato: manca il when *)
  35          | C.Fix (_,ifl) ->
  36             let counter = ref 0 in
  37              List.rev_map
  38               (function (name,_,ty,bo) ->
  39                 let res = Some (C.Name name, (C.Def (C.Fix (!counter,ifl)))) in
  40                  incr counter ;
  41                  res
  42               ) ifl
  43          | C.CoFix (_,ifl) ->
  44             let counter = ref 0 in
  45              List.rev_map
  46               (function (name,ty,bo) ->
  47                 let res = Some (C.Name name,(C.Def (C.CoFix (!counter,ifl)))) in
  48                  incr counter ;
  49                  res
  50               ) ifl
  51        in
  52         binding@(aux parentid)
  53   in
  54    aux
  55 ;;
  56
  57 exception NotImplemented;;
  58
  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
  64    let metasenv =
  65     match !P.proof with
  66        None -> assert false
  67      | Some (_,metasenv,_,_) -> metasenv
  68    in
  69     let ty = CicTypeChecker.type_of_aux' metasenv context term in
  70      P.perforate context term ty (* P.perforate also sets the goal *)
  71 ;;
  72
  73 exception FocusOnlyOnMeta;;
  74
  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
  80    let metasenv =
  81     match !P.proof with
  82        None -> assert false
  83      | Some (_,metasenv,_,_) -> metasenv
  84    in
  85     let ty = CicTypeChecker.type_of_aux' metasenv context term in
  86      match term with
  87         Cic.Meta (n,_) -> P.goal := Some n
  88       | _ -> raise FocusOnlyOnMeta
  89 ;;