From bea50d8a7fdf4063d8bf42d2983734190457e030 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Tue, 21 May 2002 15:22:26 +0000 Subject: [PATCH] *** empty log message *** --- helm/gTopLevel/gTopLevel.ml | 49 ++++++----- helm/gTopLevel/mquery.ml | 170 +++++++++++++++++++----------------- helm/gTopLevel/mquery.mli | 9 +- 3 files changed, 124 insertions(+), 104 deletions(-) diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index 083bbc7eb..789a65ba5 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -990,31 +990,38 @@ let locate rendering_window () = let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in let inputlen = inputt#length in let input = inputt#get_chars 0 inputlen in - try - output_html outputhtml (Mquery.locate input) ; - inputt#delete_text 0 inputlen - with - e -> - output_html outputhtml - ("

" ^ Printexc.to_string e ^ "

") + output_html outputhtml ( + try + match Str.split (Str.regexp "[ \t]+") input with + | [] -> "" + | head :: tail -> + inputt#delete_text 0 inputlen; + Mquery.locate head + with + e -> "

" ^ Printexc.to_string e ^ "

" + ) ;; let backward rendering_window () = let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in - let metasenv = - match !ProofEngine.proof with - None -> assert false - | Some (_,metasenv,_,_) -> metasenv - in - let result = - match !ProofEngine.goal with - | None -> "" - | Some metano -> - let (_,_,ty) = - List.find (function (m,_,_) -> m=metano) metasenv - in - Mquery.backward ty - in + let inputt = (rendering_window#inputt : GEdit.text) in + let inputlen = inputt#length in + let input = inputt#get_chars 0 inputlen in + let level = int_of_string input in + let metasenv = + match !ProofEngine.proof with + None -> assert false + | Some (_,metasenv,_,_) -> metasenv + in + let result = + match !ProofEngine.goal with + | None -> "" + | Some metano -> + let (_,_,ty) = + List.find (function (m,_,_) -> m=metano) metasenv + in + Mquery.backward ty level + in output_html outputhtml result let choose_selection diff --git a/helm/gTopLevel/mquery.ml b/helm/gTopLevel/mquery.ml index 316588f2c..e27c8e2c0 100644 --- a/helm/gTopLevel/mquery.ml +++ b/helm/gTopLevel/mquery.ml @@ -72,9 +72,9 @@ let con s = "\"" ^ s ^ "\" " let res s = "\"" ^ s ^ "\" " -let nl = "
" +let nl () = "
" -let par = "

" +let par () = "

" (* HTML representation of a query *) @@ -108,7 +108,8 @@ let rec out_bool = function let rec 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 + | 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 ")" @@ -116,6 +117,17 @@ let rec out_list = function 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 = @@ -149,18 +161,18 @@ let tref_uref (u, i) = (* CIC term inspecting functions *) -let out_ie (r, b) = - let pos = if b then "HEAD: " else "TAIL: " in - res (pos ^ str_uref r) ^ nl ^ - con (pos ^ str_tref (tref_uref r)) ^ nl +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) = (tref_uref r, b) +let tie_uie (r, b, v) = (tref_uref r, b, v) -let ie_eq ((u1, f1), b1) ((u2, f2), b2) = +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 @@ -168,69 +180,77 @@ 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 t c = - let fi = +let level = ref 0 + +let inspect_uri main l uri t c v = + if v > !level then l else + let fi = match (t, c) with | (None, _) -> (None, None) | (Some t0, c0) -> (Some (t0 + 1), c0) - in - ie_insert ((uri, fi), main) l + in + ie_insert ((uri, fi), main, v) l -let rec inspect_term main l = function +let rec inspect_term main l v = function | Rel i -> l - | Meta (i,_) -> l + | Meta (i, _) -> l | Sort s -> l | Implicit -> l | Abst u -> l - | Var u -> inspect_uri main l u None None - | Const (u, i) -> inspect_uri main l u None None - | MutInd (u, i, t) -> inspect_uri main l u (Some t) None - | MutConstruct (u, i, t, c) -> inspect_uri main l u (Some t) (Some c) + | 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, tt) -> - let luu = inspect_term main l uu in - inspect_term false luu tt + let luu = inspect_term main l (v + 1) uu in + inspect_term false luu (v + 1) tt | Prod (n, uu, tt) -> - let luu = inspect_term false l uu in - inspect_term false luu 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 uu in - inspect_term false luu 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 uu in - inspect_term false luu tt - | Appl m -> inspect_list main l m + let luu = inspect_term false l (v + 1) uu in + inspect_term false luu (v + 1) tt + | Appl m -> inspect_list main l (v + 1) m | MutCase (u, i, t, tt, uu, m) -> - let lu = inspect_uri main l u (Some t) None in - let ltt = inspect_term false lu tt in - let luu = inspect_term false ltt uu in - inspect_list main luu m - | Fix (i, m) -> inspect_ind l m - | CoFix (i, m) -> inspect_coind l m -and inspect_list main l = function + 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 (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 v = function | [] -> l | tt :: m -> - let ltt = inspect_term main l tt in - inspect_list false ltt m -and inspect_ind l = function + let ltt = inspect_term main l v tt in + inspect_list false ltt v m +and inspect_ind l v = function | [] -> l | (n, i, tt, uu) :: m -> - let ltt = inspect_term false l tt in - let luu = inspect_term false ltt uu in - inspect_ind luu m -and inspect_coind l = function + 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 tt in - let luu = inspect_term false ltt uu in - inspect_coind luu 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 [] t +let inspect t = inspect_term true [] 0 t (* query building functions *) -let build_select (r, b) n = - let rvar = "uri" ^ string_of_int n in - let svar = "s" ^ string_of_int n in +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), @@ -242,38 +262,30 @@ let rec build_inter n = function | [ie] -> build_select ie n | ie :: il -> MQIntersect (build_select ie n, build_inter (n + 1) il) +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 locate_aux txt = - let query = - MQList (MQSelect ("uri", - MQPattern ("cic", [MQAstAst], "con", (None, None)), - MQIs (MQFunc (MQName, "uri"), - MQCons txt - ) - ) - ) - in - match Mqint.execute query with - MQStrUri l -> - out_query query ^ nl ^ "Result: " ^ nl ^ - String.concat nl l ^ nl - | MQRefs _ -> assert false (*CSC: ????????????????????????????? *) + let query = + MQList (MQSelect ("ref", + MQPattern ("cic", [MQAstAst], "con", (None, None)), + MQIs (MQFunc (MQName, "ref"), + MQCons s + ) + ) + ) in - match Str.split (Str.regexp "[ \t]+") s with - | [] -> "" - | head :: tail -> par ^ locate_aux head -;; + build_result query -let backward t = +let backward t n = + level := n; let uil = inspect t in let til = List.map tie_uie uil in - let query = MQList (build_inter 0 til) in - match Mqint.execute query with - MQStrUri l -> - par ^ out_query query ^ nl ^ (* ^ par ^ out_il uil ^ *) - "Result: " ^ nl ^ String.concat nl l ^ nl - | MQRefs _ -> assert false (*CSC: ????????????????????????????? *) -;; - -let init = Mqint.init;; -let close = Mqint.close;; + let query = MQList (build_inter 0 til) in + par () ^ out_il uil ^ build_result query diff --git a/helm/gTopLevel/mquery.mli b/helm/gTopLevel/mquery.mli index bfdf89597..3ea31b8d2 100644 --- a/helm/gTopLevel/mquery.mli +++ b/helm/gTopLevel/mquery.mli @@ -39,9 +39,10 @@ val out_query : Mathql.mquery -> string (* HTML representation of a query val tref_uref : Mathql.mquref -> Mathql.mqtref (* "tref of uref" conversion *) -val locate : string -> string (* LOCATE query building function *) +val init : unit -> unit (* INIT database function *) + +val close : unit -> unit (* CLOSE database function *) -val backward : Cic.term -> string (* BACKWARD query building function *) +val locate : string -> string (* LOCATE query building function *) -val init : unit -> unit -val close : unit -> unit +val backward : Cic.term -> int -> string (* BACKWARD query building function *) -- 2.39.2