" +(* CIC term inspecting functions ********************************************) -(* 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 rec il_max = function + | [] -> 0 + | (_, _, v) :: tail -> + let v0 = il_max tail in + if v > v0 then v else v0 + +let ie_str_uri (u, b, v) = xp_str_uref u let rec il_restrict level = function | [] -> [] @@ -36,80 +74,106 @@ let rec ie_insert ie = 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 *************************************************) -(* query building functions *) +let issue = ref (fun _ -> true) let save s = let och = open_out_gen [Open_wronly; Open_append; Open_creat; Open_text] (64 * 6 + 8 * 6 + 4) "MQGenLog.htm" in output_string och s; flush och; s +let build_result query = + if ! issue query then + let html = par () ^ out_query query ^ nl () in + let result = Mqint.execute query in + save (html ^ out_result result) + else "" + let build_select (r, b, v) n = let rvar = "ref" ^ string_of_int n in 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) @@ -118,7 +182,7 @@ let restrict_universe query = [] -> 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, @@ -138,33 +202,50 @@ let restrict_universe query = ) ) -let build_result query = - let html = par () ^ out_query query ^ nl () in - let result = Mqint.execute query in - save (html ^ out_result result) - let init = Mqint.init let close = Mqint.close -let locate s = - let query = +let locate_query s = (*CSC: next query to be fixed 1) I am exploiting the bug that does not quote '|' 2) I am searching only constants and mutual inductive definition blocks (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 locate s = + (*CSC: the code should be: Mqint.execute (locate_query s) *) + (*CSC: what follows is the patch to map mutual inductive definition blocks *) + (*CSC: URIs (i.e. no fragment identifier at all) to the URIs of the first *) + (*CSC: mutual inductive type of their block. *) + let MQRefs uris = Mqint.execute (locate_query s) in + MQRefs + (List.map + (function uri -> + if String.sub uri (String.length uri - 4) 4 = ".con" then uri else + uri ^ "#1/1" + ) uris) +;; + +let locate_html s = build_result (locate_query s);; + +let levels e c t = + env := e; cont := c; + let il = inspect t in + par () ^ il_out il ^ nl () + +let call_back f = + issue := f + +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