" - -(* HTML representation of a query *) - -let out_rvar s = sym s - -let out_svar s = sep "$" ^ sym s - -let out_tref r = con (str_tref r) - -let out_pat p = out_tref p - -let out_func = function - | MQName -> key "name" - | _ -> assert false - -let out_str = function - | MQCons s -> con s - | MQRVar s -> out_rvar s - | MQSVar s -> out_svar s - | MQFunc (f, r) -> out_func f ^ out_rvar r - | MQMConclusion -> key "mainconclusion" - | MQConclusion -> key "conclusion" - -let rec out_bool = function - | MQTrue -> key "true" - | MQFalse -> key "false" - | MQIs (s, t) -> out_str s ^ key "is" ^ out_str t - | MQNot b -> key "not" ^ out_bool b - | MQAnd (b1, b2) -> sep "(" ^ out_bool b1 ^ key "and" ^ out_bool b2 ^ sep ")" - | MQOr (b1, b2) -> sep "(" ^ out_bool b1 ^ key "or" ^ out_bool b2 ^ sep ")" - | MQSetEqual (l1, l2) -> - sep "(" ^ out_list l1 ^ key "setequal" ^ out_list l2 ^ sep ")" - | MQSubset (l1, l2) -> - sep "(" ^ out_list l1 ^ key "subset" ^ out_list l2 ^ sep ")" - -and out_list = function - | MQSelect (r, l, b) -> - key "select" ^ out_rvar r ^ key "in" ^ out_list l ^ key "where" ^ out_bool b - | MQUse (l, v) -> key "use" ^ out_list l ^ key "position" ^ out_svar v - | MQUsedBy (l, v) -> key "usedby" ^ out_list l ^ key "position" ^ out_svar v - | MQPattern p -> key "pattern" ^ out_pat p - | MQUnion (l1, l2) -> sep "(" ^ out_list l1 ^ key "union" ^ out_list l2 ^ sep ")" - | MQIntersect (l1, l2) -> sep "(" ^ out_list l1 ^ key "intersect" ^ out_list l2 ^ sep ")" - | MQRVarOccur v -> key "rvaroccur" ^ v - -let out_query = function - | MQList l -> out_list l - -(* HTML representation of a query result *) - -let rec out_list = function - | [] -> "" - | u :: l -> res (str_tref u) ^ nl () ^ out_list l - -let out_result qr = - par () ^ "Result:" ^ nl () ^ - match qr with - | MQRefs l -> out_list l - -(* Converting functions *) - -let split s = - try - let i = Str.search_forward (Str.regexp_string ":/") s 0 in - let p = Str.string_before s i in - let q = Str.string_after s (i + 2) in - (p, q) - with - Not_found -> (s, "") - -let encode = function - | Str.Text s -> MQString s - | Str.Delim s -> - if s = "?" then MQAnyChr else - if s = "*" then MQAst else - if s = "**" then MQAstAst else - if s = "/" then MQSlash else MQString s - -let tref_uref (u, i) = - let s = UriManager.string_of_uri u in - match split s with - | (p, q) -> - let rx = Str.regexp "\?\|\*\*\|\*\|/" in - let l = Str.full_split rx q in - (p, List.map encode l, i) - -(* CIC term inspecting functions *) - -let out_ie (r, b, v) = - let pos = string_of_int v ^ if b then " HEAD: " else " TAIL: " in - res (pos ^ str_uref r) ^ nl () ^ - con (pos ^ str_tref (tref_uref r)) ^ nl () - -let rec out_il = function - | [] -> "" - | head :: tail -> out_ie head ^ out_il tail - -let tie_uie (r, b, v) = (tref_uref r, b, v) - -let ie_eq ((u1, f1), b1, v1) ((u2, f2), b2, v2) = - UriManager.eq u1 u2 && f1 = f2 && b1 = b2 - -let rec ie_insert ie = function - | [] -> [ie] - | head :: tail -> - head :: if ie_eq head ie then tail else ie_insert ie tail - -let level = ref 0 - -(*CSC: che brutto il codice imperativo!!!*) -let universe = ref [];; - -let inspect_uri main l uri t c v = - let fi = - match (t, c) with - | (None, _) -> (None, None) - | (Some t0, c0) -> (Some (t0 + 1), c0) - in -(*CSC: sbagliato, credo. MQString non dovrebbe poter contenere slash *) - universe := (tref_uref (uri,fi))::!universe ; - if v > !level then - l - else - ie_insert ((uri, fi), main, v) l -;; - -let rec inspect_term main l v = function - | Rel i -> l - | Meta (i, _) -> l - | Sort s -> l - | Implicit -> l - | Abst u -> l - | Var u -> inspect_uri main l u None None v - | Const (u, i) -> inspect_uri main l u None None v - | MutInd (u, i, t) -> inspect_uri main l u (Some t) None v - | MutConstruct (u, i, t, c) -> inspect_uri main l u (Some t) (Some c) v - | 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) -> - let luu = inspect_term false l (v + 1) uu in - inspect_term false luu (v + 1) tt - | Lambda (n, uu, tt) -> - let luu = inspect_term false l (v + 1) uu in - inspect_term false luu (v + 1) tt - | LetIn (n, 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 (Some t) None (v + 1) 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 -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 - inspect_list false ltt false v m -and inspect_ind l v = function - | [] -> l - | (n, i, 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 -> - 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 - -(* query building functions *) - -let save s = - let och = open_out_gen [Open_wronly; Open_append; Open_creat; Open_text] - (64 * 6 + 8 * 6 + 4) "mquery.htm" in - output_string och s; flush och; s - -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 (MQPattern r, svar), - MQIs (MQSVar svar, mqs) - ) - -let rec build_inter n = function - | [] -> MQPattern ("cic", [MQAstAst; MQString ".con"], (None, None)) - | [ie] -> build_select ie n - | ie :: il -> MQIntersect (build_select ie n, build_inter (n + 1) il) - -let restrict_universe query = - function - [] -> query (* no constraints ===> the universe is the library *) - | l -> - let universe = - (*CSC: Usare tante Union e Pattern per fare un insieme di uri mi *) - (*CSC: sembra un poco penoso. Inoltre creo un albero completamente *) - (*CSC: sbilanciato, aumentando il costo della risoluzione della *) - (*CSC: query. *) - let rec compose_universe = - function - [] -> assert false - | [uri] -> MQPattern uri - | uri::tl -> MQUnion(MQPattern uri, compose_universe tl) - in - compose_universe !universe - in - MQSelect ( - "uri", query, - MQSubset ( - MQSelect ( - "uri2", - MQUsedBy (MQRVarOccur "uri", "pos"), - MQOr ( - MQIs (MQSVar "pos", MQConclusion), - MQIs (MQSVar "pos", MQMConclusion) - ) - ), - universe - ) - ) -;; - -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 = - MQList (MQSelect ("ref", - MQPattern ("cic", [MQAstAst; MQString ".con"], (None, None)), - MQIs (MQFunc (MQName, "ref"), - MQCons s - ) - ) - ) - in - build_result query - -let backward t n = - level := n ; - universe := [] ; - let uil = inspect t in - let til = List.map tie_uie uil in - let query = build_inter 0 til in - let query' = restrict_universe query til in - let query'' = MQList query' in - par () ^ out_il uil ^ build_result query'' -;;