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 P = ProofEngine in
   9  let module C = Cic in
  10   let rec aux id =
  11    match get_parent id ids_to_terms ids_to_father_ids with
  12       None -> []
  13     | Some (parentid,parent) ->
  14        let term = Hashtbl.find ids_to_terms id in
  15        let binding =
  16         match parent with
  17            C.Rel _
  18          | C.Var _
  19          | C.Meta _
  20          | C.Sort _
  21          | C.Implicit
  22          | C.Cast _ -> []
  23          | C.Prod (n,s,t) when t == term -> [P.Declaration (n,s)]
  24          | C.Prod _ -> []
  25          | C.Lambda (n,s,t) when t == term -> [P.Declaration (n,s)]
  26          | C.Lambda _ -> []
  27          | C.LetIn (n,s,t) when t == term -> [P.Definition (n,s)]
  28          | C.LetIn _ -> []
  29          | C.Appl _
  30          | C.Const _ -> []
  31          | C.Abst _ -> assert false
  32          | C.MutInd _
  33          | C.MutConstruct _
  34          | C.MutCase _ -> []
  35 (*CSC: sbagliato: manca il when *)
  36          | C.Fix (_,ifl) ->
  37             let counter = ref 0 in
  38              List.rev_map
  39               (function (name,_,ty,bo) ->
  40                 let res = (P.Definition (C.Name name, C.Fix (!counter,ifl))) in
  41                  incr counter ;
  42                  res
  43               ) ifl
  44          | C.CoFix (_,ifl) ->
  45             let counter = ref 0 in
  46              List.rev_map
  47               (function (name,ty,bo) ->
  48                 let res = (P.Definition (C.Name name, C.CoFix (!counter,ifl))) in
  49                  incr counter ;
  50                  res
  51               ) ifl
  52        in
  53         binding@(aux parentid)
  54   in
  55    aux
  56 ;;
  57
  58 exception NotImplemented;;
  59
  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 metasenv =
  67     match !P.proof with
  68        None -> assert false
  69      | Some (_,metasenv,_,_) -> metasenv
  70    in
  71     let ty =
  72      CicTypeChecker.type_of_aux' metasenv
  73       (P.cic_context_of_named_context context) term
  74     in
  75      let (meta,perforated) =
  76       (* If the selected term is already a meta, we return it. *)
  77       (* Otherwise, we are trying to refine a non-meta term... *)
  78       match term with
  79          Cic.Meta n -> P.goal := Some (n,(context,ty)) ; n,false
  80        | _ -> P.perforate context term ty,true (* P.perforate also sets the goal *)
  81      in
  82       perforated
  83 ;;