+++ /dev/null
-open MathQL
-open Cic
-
-(* string linearization of a reference *)
-
-let str_uptoken = function
- | MQBC s -> s
- | MQBD -> "/"
- | MQBQ -> "?"
- | MQBS -> "*"
- | MQBSS -> "**"
-
-let rec str_up = function
- | [] -> ""
- | head :: tail -> str_uptoken head ^ str_up tail
-
-let str_fi fi =
- "#1/" ^
- String.concat "/"
- (List.map
- (function
- MQFC n -> string_of_int n
- | MQFS -> "*"
- | MQFSS -> "**"
- ) fi)
-
- function
- | (None, _) -> ""
- | (Some t, None) -> "#1/" ^ string_of_int t
- | (Some t, Some c) -> "#1/" ^ string_of_int t ^ "/" ^ string_of_int c
-
-let str_tref (p, u, i) =
- let p =
- match p with
- None -> "*"
- | Some s -> s
- in
- p ^ ":/" ^ str_up u ^ str_fi i
-
-let str_uref (u, i) =
- UriManager.string_of_uri u ^ str_fi i
-
-(* raw HTML representation *)
-
-let key s = "<font color=\"blue\">" ^ s ^ " </font>"
-
-let sym s = s ^ " "
-
-let sep s = s
-
-let con s = "<font color=\"red\">\"" ^ s ^ "\" </font>"
-
-let res s = "<font color=\"brown\">\"" ^ s ^ "\" </font>"
-
-let nl () = "<br>"
-
-let par () = "<p>"
-
-(* 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
- | MQStringRVar s -> out_rvar s
- | MQStringSVar 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 ")"
- | MQListRVar v -> key "rvaroccur" ^ v
- | MQLetIn (v, l1, l2) ->
- key "let " ^ out_rvar v ^ " = " ^ out_list l1 ^ key " in " ^ out_list l2
- | MQListLVar v -> out_rvar v
-
-let out_query = function
- | MQList l -> out_list l
-
-(* HTML representation of a query result *)
-
-let rec out_list = function
- | [] -> ""
- | u :: l -> res 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 -> MQBC s
- | Str.Delim s ->
- if s = "?" then MQBQ else
- if s = "*" then MQBS else
- if s = "**" then MQBSS else
- if s = "/" then MQBD else MQBC 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
- (Some 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, _) -> []
- | (Some t0, Some c0) -> [MQFC (t0 + 1); MQFC c0]
- | (Some t0, None) -> [MQFC (t0 + 1)]
- 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
- | 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 (MQStringSVar svar, mqs)
- )
-
-let rec build_inter n = function
- | [] -> MQPattern (Some "cic", [MQBSS; MQBC ".con"], [])
- | [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
- MQLetIn (
- "universe",universe,
- MQSelect (
- "uri", query,
- MQSubset (
- MQSelect (
- "uri2",
- MQUsedBy (MQListRVar "uri", "pos"),
- MQOr (
- MQIs (MQStringSVar "pos", MQConclusion),
- MQIs (MQStringSVar "pos", MQMConclusion)
- )
- ),
- MQListLVar "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 (Some "cic", [MQBSS ; MQBC ".con"], []),
- 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''
-;;
projects / helm.git / commitdiff