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.MutInd _
  31          | C.MutConstruct _
  32          | C.MutCase _ -> []
  33 (*CSC: sbagliato: manca il when *)
  34          | C.Fix (_,ifl) ->
  35             let counter = ref 0 in
  36              List.rev_map
  37               (function (name,_,ty,bo) ->
  38                 let res = Some (C.Name name, (C.Def (C.Fix (!counter,ifl)))) in
  39                  incr counter ;
  40                  res
  41               ) ifl
  42          | C.CoFix (_,ifl) ->
  43             let counter = ref 0 in
  44              List.rev_map
  45               (function (name,ty,bo) ->
  46                 let res = Some (C.Name name,(C.Def (C.CoFix (!counter,ifl)))) in
  47                  incr counter ;
  48                  res
  49               ) ifl
  50        in
  51         binding@(aux parentid)
  52   in
  53    aux
  54 ;;
  55
  56 exception NotImplemented;;
  57
  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
  63    let metasenv =
  64     match !P.proof with
  65        None -> assert false
  66      | Some (_,metasenv,_,_) -> metasenv
  67    in
  68     let ty = CicTypeChecker.type_of_aux' metasenv context term in
  69      P.perforate context term ty (* P.perforate also sets the goal *)
  70 ;;
  71
  72 exception FocusOnlyOnMeta;;
  73
  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
  79    let metasenv =
  80     match !P.proof with
  81        None -> assert false
  82      | Some (_,metasenv,_,_) -> metasenv
  83    in
  84     let ty = CicTypeChecker.type_of_aux' metasenv context term in
  85      match term with
  86         Cic.Meta (n,_) -> P.goal := Some n
  87       | _ -> raise FocusOnlyOnMeta
  88 ;;