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 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 type_checker_env_of_context =
  65     List.map
  66      (function
  67          P.Declaration,_,t -> t
  68        | P.Definition,_,_ -> raise NotImplemented
  69      ) context
  70    in
  71     let ty = CicTypeChecker.type_of_aux' type_checker_env_of_context term in
  72      ((context,ty) : ProofEngine.sequent)
  73 ;;