(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
*)
+module T = MQGTypes
+
let text_of_entries out entries =
out "(** MatchConclusion: results of the term inspection **)\n";
let text_of_entry (u, b, v) =
let levels_of_term metasenv context term =
let module TC = CicTypeChecker in
let module Red = CicReduction in
- let module Util = MQueryUtil in
let degree t =
let rec degree_aux = function
| Cic.Sort _ -> 1
| Cic.Prod (_, _, t) -> degree_aux t
| _ -> 2
in
- let u = TC.type_of_aux' metasenv context t in
+ let u,_ = TC.type_of_aux' metasenv context t CicUniv.empty_ugraph in
degree_aux (Red.whd context u)
in
let entry_eq (s1, b1, v1) (s2, b2, v2) =
in
let inspect_uri main l uri tc v term =
let d = degree term in
- entry_in (Util.string_of_uriref (uri, tc), main, 2 * v + d - 1) l
+ entry_in (UriManager.string_of_uriref (uri, tc), main, 2 * v + d - 1) l
in
let rec inspect_term main l v term = match term with
Cic.Rel _ -> l
| Cic.Meta _ -> l
| Cic.Sort _ -> l
- | Cic.Implicit -> l
+ | Cic.Implicit _ -> l
| Cic.Var (u,exp_named_subst) ->
- let l' = inspect_uri main l u [] v term in
+ inspect_exp_named_subst l (succ v) exp_named_subst
+(*
+ let l' = inspect_uri main l u [] v term in
inspect_exp_named_subst l' (succ v) exp_named_subst
+*)
| Cic.Const (u,exp_named_subst) ->
let l' = inspect_uri main l u [] v term in
inspect_exp_named_subst l' (succ v) exp_named_subst
mk_musts (prev @ [acc]) acc next
in
mk_musts [] [] can
-(*
- let uri_pos (u,b,v) = (u,b) in
- let can_use = List.map uri_pos can in
- let lofl (u,b,v) = [(u,b)] in
- let rec organize_restr rlist prev_r=
- match rlist with
- [] -> []
- | r::tl ->let curr_r = r@prev_r in
- curr_r::(organize_restr tl curr_r)
- in
- let mrest = List.map lofl can in
- let must_use = organize_restr mrest [] in (* must restrictions *)
- (must_use,can_use)
-*)
+
+let universe = [T.MainConclusion; T.InConclusion]