(* CIC term inspecting functions *)
+let env = ref [] (* metasemv *)
+let cont = ref [] (* context *)
+
let ie_out (r, b, v) =
let pos = string_of_int v ^ if b then " HEAD: " else " TAIL: " in
- res (pos ^ str_uref r) ^ nl ()
+ res (pos ^ str_uref r) ^ nl () (* FG: si puo' usare xp_str_uref se si vuole xpointer *)
let rec il_out = function
| [] -> ""
| head :: tail -> ie_out head ^ il_out tail
-let ie_struri (u, b, v) = str_uref u
+let ie_str_uri (u, b, v) = xp_str_uref u
let rec il_restrict level = function
| [] -> []
| head :: tail ->
head :: if ie_eq head ie then tail else ie_insert ie tail
-let inspect_uri main l uri tc v =
+let degree t =
+ let u0 = CicTypeChecker.type_of_aux' !env !cont t in
+ let u = CicReduction.whd !cont u0 in
+ let rec deg = function
+ | Sort _ -> 1
+ | Cast (uu, _) -> deg uu
+ | Prod (_, _, tt) -> deg tt
+ | _ -> 2
+ in deg u
+
+let inspect_uri main l uri tc v term =
+ let d = degree term in
let fi = match tc with
| t0 :: c0 :: _ -> [t0 + 1; c0]
| t0 :: _ -> [t0 + 1]
| [] -> []
- in ie_insert ((uri, fi), main, v) l
+ in ie_insert ((uri, fi), main, 2 * v + d - 1) l
-let rec inspect_term main l v = function
- | Rel i -> l
- | Meta (i, _) -> l
- | Sort s -> l
+let rec inspect_term main l v term =
+ match term with
+ | Rel _ -> l
+ | Meta (_, _) -> l
+ | Sort _ -> l
| Implicit -> l
- | Var u -> inspect_uri main l u [] v
- | Const (u, i) -> inspect_uri main l u [] v
- | MutInd (u, i, t) -> inspect_uri main l u [t] v
- | MutConstruct (u, i, t, c) -> inspect_uri main l u [t; c] v
+ | Var u -> inspect_uri main l u [] v term
+ | Const (u, _) -> inspect_uri main l u [] v term
+ | MutInd (u, _, t) -> inspect_uri main l u [t] v term
+ | MutConstruct (u, _, t, c) -> inspect_uri main l u [t; c] v term
| Cast (uu, _) ->
- (*CSC: Cast modified so that it behaves exactly as if no Cast was there *)
inspect_term main l v uu
- | Prod (n, uu, tt) ->
+ | Prod (_, uu, tt) ->
let luu = inspect_term false l (v + 1) uu in
- inspect_term false luu (v + 1) tt
- | Lambda (n, uu, tt) ->
+ inspect_term main luu (v + 1) tt
+ | Lambda (_, uu, tt) ->
let luu = inspect_term false l (v + 1) uu in
inspect_term false luu (v + 1) tt
- | LetIn (n, uu, tt) ->
+ | LetIn (_, uu, tt) ->
let luu = inspect_term false l (v + 1) uu in
inspect_term false luu (v + 1) tt
| Appl m -> inspect_list main l true v m
- | MutCase (u, i, t, tt, uu, m) ->
- let lu = inspect_uri main l u [t] (v + 1) in
+ | MutCase (u, _, t, tt, uu, m) ->
+ let lu = inspect_uri main l u [t] (v + 1) term in
let ltt = inspect_term false lu (v + 1) tt in
let luu = inspect_term false ltt (v + 1) uu in
inspect_list main luu false (v + 1) m
- | Fix (i, m) -> inspect_ind l (v + 1) m
- | CoFix (i, m) -> inspect_coind l (v + 1) m
+ | Fix (_, m) -> inspect_ind l (v + 1) m
+ | CoFix (_, m) -> inspect_coind l (v + 1) m
and inspect_list main l head v = function
| [] -> l
| tt :: m ->
- let ltt = inspect_term main l (if head then v else v+1) tt in
+ let ltt = inspect_term main l (if head then v else v + 1) tt in
inspect_list false ltt false v m
and inspect_ind l v = function
| [] -> l
- | (n, i, tt, uu) :: m ->
+ | (_, _, tt, uu) :: m ->
let ltt = inspect_term false l v tt in
let luu = inspect_term false ltt v uu in
inspect_ind luu v m
and inspect_coind l v = function
| [] -> l
- | (n, tt, uu) :: m ->
+ | (_, tt, uu) :: m ->
let ltt = inspect_term false l v tt in
let luu = inspect_term false ltt v uu in
inspect_coind luu v m
-let inspect t = inspect_term true [] 0 t
+let rec inspect_backbone = function
+ | Cast (uu, _) -> inspect_backbone uu
+ | Prod (_, _, tt) -> inspect_backbone tt
+ | LetIn (_, uu, tt) -> inspect_backbone tt
+ | t -> inspect_term true [] 0 t
+
+let inspect t = inspect_backbone t
(* query building functions *)
let svar = "str" ^ string_of_int n in
let mqs = if b then MQMConclusion else MQConclusion in
MQSelect (rvar,
- MQUse (MQReference [str_uref r], svar),
+ MQUse (MQReference [xp_str_uref r], svar),
MQIs (MQStringSVar svar, mqs)
)
let rec build_inter n = function
- | [] -> MQPattern [(None, [MQBSS], [MQFSS])]
+ | [] -> MQPattern (None, [MQBSS], [MQFSS])
| [ie] -> build_select ie n
| ie :: il -> MQIntersect (build_select ie n, build_inter (n + 1) il)
[] -> query (* no constraints ===> the universe is the library *)
| l ->
let universe =
- MQReference (List.map ie_struri l)
+ MQReference (List.map ie_str_uri l)
in
MQLetIn (
"universe", universe,
(i.e. no fragment identifier at all)
*)
MQList (MQSelect ("ref",
- MQPattern [(Some "cic", [MQBSS ; MQBC ".con|.ind"],[])],
+ MQPattern (Some "cic", [MQBSS ; MQBC ".con|.ind"],[]),
MQIs (MQFunc (MQName, "ref"),
MQCons s
)
in
build_result query
-let backward t level =
+let levels e c t level =
+ env := e; cont := c;
+ let il = inspect t in
+ par () ^ il_out il ^ nl ()
+
+let backward e c t level =
+ env := e; cont := c;
let il = inspect t in
let query = build_inter 0 (il_restrict level il) in
let query' = restrict_universe query il in
projects / helm.git / blobdiff