(*CSC: We save the innertypes to disk so that we can retrieve them in the *)
(*CSC: stylesheet. This DOES NOT work when UWOBO and/or the getter are not *)
(*CSC: local. *)
- Xml.pp xmlinnertypes (Some "/public/sacerdot/innertypes") ;
+ Xml.pp xmlinnertypes (Some "/home/fguidi/innertypes") ;
let output = applyStylesheets input mml_styles mml_args in
output
;;
match !ProofEngine.goal with
| None -> ""
| Some metano ->
- let (_,_,ty) =
+ let (_, ey ,ty) =
List.find (function (m,_,_) -> m=metano) metasenv
in
- MQueryGenerator.backward ty level
+ MQueryGenerator.backward metasenv ey ty level
in
output_html outputhtml result
(* 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
(* *)
(******************************************************************************)
-val init : unit -> unit (* INIT database function *)
+val levels : Cic.metasenv -> Cic.context -> Cic.term -> int -> string
+ (* level assignment testing function *)
-val close : unit -> unit (* CLOSE database function *)
+val init : unit -> unit (* INIT database function *)
-val locate : string -> string (* LOCATE query building function *)
+val close : unit -> unit (* CLOSE database function *)
-val backward : Cic.term -> int -> string (* BACKWARD query building function *)
+val locate : string -> string (* LOCATE query building function *)
+
+val backward : Cic.metasenv -> Cic.context -> Cic.term -> int -> string
+ (* BACKWARD query building function *)
--- /dev/null
+BIN_DIR = /usr/local/bin
+REQUIRES = helm-cic_textual_parser helm-cic_proof_checking helm-mathql helm-mathql_interpreter
+PREDICATES =
+OCAMLOPTIONS = -I .. -package "$(REQUIRES)" -predicates "$(PREDICATES)"
+OCAMLC = ocamlfind ocamlc $(OCAMLOPTIONS)
+OCAMLOPT = ocamlfind ocamlopt $(OCAMLOPTIONS)
+OCAMLDEP = ocamldep
+
+LIBRARIES = $(shell ocamlfind query -recursive -predicates "byte $(PREDICATES)" -format "%d/%a" $(REQUIRES))
+LIBRARIES_OPT = $(shell ocamlfind query -recursive -predicates "native $(PREDICATES)" -format "%d/%a" $(REQUIRES))
+
+all: topLevel
+opt: topLevel.opt
+
+DEPOBJS = topLevel.ml
+
+TOPLEVELOBJS = ../mQueryGenerator.cmo topLevel.cmo
+
+depend:
+ $(OCAMLDEP) $(DEPOBJS) > .depend
+
+topLevel: $(TOPLEVELOBJS) $(LIBRARIES)
+ $(OCAMLC) -linkpkg -o topLevel $(TOPLEVELOBJS)
+
+topLevel.opt: $(TOPLEVELOBJS:.cmo=.cmx) $(LIBRARIES_OPT)
+ $(OCAMLOPT) -linkpkg -o topLevel.opt $(TOPLEVELOBJS:.cmo=.cmx)
+
+.SUFFIXES: .ml .mli .cmo .cmi .cmx
+.ml.cmo: $(LIBRARIES)
+ $(OCAMLC) -c $<
+.mli.cmi: $(LIBRARIES)
+ $(OCAMLC) -c $<
+.ml.cmx: $(LIBRARIES_OPT)
+ $(OCAMLOPT) -c $<
+
+clean:
+ rm -f *.cm[iox] *.o topLevel topLevel.opt
+
+install:
+ cp topLevel topLevel.opt $(BIN_DIR)
+
+uninstall:
+ rm -f $(BIN_DIR)/topLevel $(BIN_DIR)/topLevel.opt
+
+.PHONY: install uninstall clean
+
+include .depend
--- /dev/null
+uso del tool topLevel
+
+Il tool e` un interfaccia testuale per mQueryGenerator che prende dati
+dallo stdin e restituisce l'output su stdout in formato html.
+L'input puo' contenere piu' di un termine CIC (usare ; per separare).
+
+Sintassi: topLevel <opzioni>
+
+Opzioni : -locate <nome> : invocazione do Locate
+ -backward <indice> : invocazione di Backward
+ -show : mostra solo i termini CIC nell'input
+ -test <indice> : mostra l'attribuzione dei livelli per
+ la backward, ma non la esegue
+
+le opzioni si possono anche scrivere -l -b -s e -t
\ No newline at end of file
--- /dev/null
+let get_terms () =
+ let terms = ref [] in
+ let lexbuf = Lexing.from_channel stdin in
+ try
+ while true do
+ match CicTextualParser.main CicTextualLexer.token lexbuf with
+ | None -> ()
+ | Some expr -> terms := expr :: ! terms
+ done;
+ ! terms
+ with
+ CicTextualParser0.Eof -> ! terms
+
+let locate name =
+ print_endline (MQueryGenerator.locate name);
+ flush stdout
+
+let rec display = function
+ | [] -> ()
+ | term :: tail ->
+ display tail;
+ print_endline ("? " ^ CicPp.ppterm term ^ "<p>");
+ flush stdout
+
+let rec levels level = function
+ | [] -> ()
+ | term :: tail ->
+ levels level tail;
+ print_endline ("? " ^ CicPp.ppterm term ^ "<p>");
+ print_endline (MQueryGenerator.levels [] [] term level);
+ flush stdout
+
+let rec backward level = function
+ | [] -> ()
+ | term :: tail ->
+ backward level tail;
+ print_endline ("? " ^ CicPp.ppterm term ^ "<p>");
+ print_endline (MQueryGenerator.backward [] [] term level);
+ flush stdout
+
+let parse_args () =
+ let rec parse = function
+ | [] -> ()
+ | ("-l"|"-locate") :: arg :: rem ->
+ locate arg; parse rem
+ | ("-d"|"-display") :: rem ->
+ display (get_terms ())
+ | ("-t"|"-test") :: arg :: rem ->
+ levels (int_of_string arg) (get_terms ())
+ | ("-b"|"-backward") :: arg :: rem ->
+ backward (int_of_string arg) (get_terms ())
+ | _ :: rem -> parse rem
+ in
+ parse (List.tl (Array.to_list Sys.argv))
+
+let _ =
+ CicCooking.init () ;
+ Logger.log_callback :=
+ (Logger.log_to_html
+ ~print_and_flush:(function s -> print_string s ; flush stdout)) ;
+ MQueryGenerator.init ();
+ parse_args ();
+ MQueryGenerator.close ();
+ exit 0
+;;
| LPR boole RPR { $2 }
;
rlist:
- | PATT REF { MQPattern [$2] }
+ | PATT REF { MQPattern $2 }
| rlist UNION rlist { MQUnion ($1, $3) }
| rlist INTER rlist { MQIntersect ($1, $3) }
| USE rlist POS svar { MQUse ($2, $4) }
| MQBS -> "*"
| MQBSS -> "**"
+let str_ftoken = function
+ | MQFC i -> string_of_int i
+ | MQFS -> "*"
+ | MQFSS -> "**"
+
let str_prot = function
| Some s -> s
| None -> "*"
| [] -> ""
| head :: tail -> str_btoken head ^ str_body tail
-let str_frag l =
- match l with
- [] -> ""
- | l ->
- let str_ftokens =
- List.fold_left
- (fun i t ->
- i ^
- match t with
- MQFC i -> "/" ^ string_of_int i
- | MQFS -> "/*"
- | MQFSS -> "/**"
- ) "" l
- in
- "#xpointer(1" ^ str_ftokens ^ ")"
-;;
+let str_frag xpointer f l =
+ let sfi = List.fold_left (fun l0 t0 -> l0 ^ "/" ^ f t0) "" l in
+ if sfi = "" then "" else
+ if xpointer then "#xpointer(1" ^ sfi ^ ")" else
+ "#1" ^ sfi
let str_tref (p, b, i) =
- str_prot p ^ ":/" ^ str_body b ^ str_frag i
-;;
+ str_prot p ^ ":/" ^ str_body b ^ str_frag false str_ftoken i
+
+let xp_str_tref (p, b, i) =
+ str_prot p ^ ":/" ^ str_body b ^ str_frag true str_ftoken i
let str_uref (u, i) =
- UriManager.string_of_uri u ^
- match i with
- [] -> ""
- | l ->
- "#xpointer(1" ^
- List.fold_left (fun i n -> i ^ "/" ^ string_of_int n) "" l ^
- ")"
-;;
+ UriManager.string_of_uri u ^ str_frag false string_of_int i
+
+let xp_str_uref (u, i) =
+ UriManager.string_of_uri u ^ str_frag true string_of_int i
(* raw HTML representation *)
let out_tref r = pat (str_tref r)
-
let rec out_sequence f = function
| [] -> sep "."
| [s] -> f s
key "select" ^ out_rvar r ^ sub "in" ^ out_list l ^ sub "where" ^ out_bool b
| MQUse (l, v) -> key "use" ^ out_list l ^ sub "position" ^ out_svar v
| MQUsedBy (l, v) -> key "usedby" ^ out_list l ^ sub "position" ^ out_svar v
- | MQPattern p -> key "pattern" ^ out_sequence out_tref p
+ | MQPattern p -> key "pattern" ^ out_tref p
| MQUnion (l1, l2) -> sep "(" ^ out_list l1 ^ sub "union" ^ out_list l2 ^ sep ")"
| MQIntersect (l1, l2) -> sep "(" ^ out_list l1 ^ sub "intersect" ^ out_list l2 ^ sep ")"
| MQDiff (l1, l2) -> sep "(" ^ out_list l1 ^ sub "diff" ^ out_list l2 ^ sep ")"
| MQListLVar v -> out_lvar v
| MQLetIn (v, l1, l2) -> key "let" ^ out_lvar v ^ sub "be" ^ out_list l1 ^ sub "in" ^ out_list l2
| MQReference s -> key "reference" ^ out_sequence str s
- | MQMinimize l -> key "minimize" ^ out_list l
let out_query = function
| MQList l -> out_list l
(* *)
(******************************************************************************)
-val str_uref : MathQL.mquref -> string (* string linearization of a UriManager reference *)
+val str_uref : MathQL.mquref -> string (* string linearization of a UriMan. reference *)
-val str_tref : MathQL.mqtref -> string (* string linearization of a tokenized reference *)
+val str_tref : MathQL.mqtref -> string (* string linearization of a tokenized reference *)
-val out_query : MathQL.mquery -> string (* HTML representation of a query *)
+val xp_str_uref : MathQL.mquref -> string (* string linearization of a UriMan. reference *)
-val out_result : MathQL.mqresult -> string (* HTML representation of a query result *)
+val xp_str_tref : MathQL.mqtref -> string (* string linearization of a tokenized reference *)
-val tref_uref : MathQL.mquref -> MathQL.mqtref (* "tref of uref" conversion *)
+val out_query : MathQL.mquery -> string (* HTML representation of a query *)
-val parse_text : in_channel -> MathQL.mquery (* textual parsing of a query *)
+val out_result : MathQL.mqresult -> string (* HTML representation of a query result *)
+
+val tref_uref : MathQL.mquref -> MathQL.mqtref (* "tref of uref" conversion *)
+
+val parse_text : in_channel -> MathQL.mquery (* textual parsing of a query *)
type mqtref = mqpt * (mqbt list) * (mqft list) (* tokenized pattern reference *)
-type mqref = string (* format for references (helper) *)
-
type mqfunc =
| MQName (* Name *)
| MQTheory (* theory *)
| MQSubset of mqlist * mqlist (* the two lists denote two sets, the 1st subset of the 2nd *)
and mqlist =
- | MQReference of mqref list (* reference list *)
- | MQPattern of mqtref list (* pattern list *)
+ | MQReference of string list (* reference list *)
+ | MQPattern of mqtref (* pattern *)
| MQListLVar of mqlvar (* lvar *)
| MQListRVar of mqrvar (* rvar *)
| MQSelect of mqrvar * mqlist * mqbool (* rvar, list, boolean *)
| MQSortedBy of mqlist * mqorder * mqfunc (* ordering *)
| MQDiff of mqlist * mqlist (* set difference *)
| MQLetIn of mqlvar * mqlist * mqlist (* explicit lvar assignment *)
- | MQMinimize of mqlist (* list minimization *)
-
+
type mquery =
| MQList of mqlist
(* main type is mqresult *)
type mqresult =
- | MQRefs of mqref list
+ | MQRefs of string list
let ll1 = string_of_int (List.length l1) in
let ll2 = string_of_int (List.length l2) in
let diff = string_of_float (after -. before) in
- prerr_endline
+ print_endline
("DIFF(" ^ ll1 ^ ", " ^ ll2 ^ ") = " ^ string_of_int (List.length res) ^
": " ^ diff ^ "s") ;
- flush stderr ;
+ flush stdout ;
res
;;
let ll1 = string_of_int (List.length l1) in
let ll2 = string_of_int (List.length l2) in
let diff = string_of_float (after -. before) in
- prerr_endline
+ print_endline
("INTERSECT(" ^ ll1 ^ "," ^ ll2 ^ ") = " ^ string_of_int (List.length res) ^
": " ^ diff ^ "s") ;
- flush stderr ;
+ flush stdout ;
res
;;
else List.assoc prop (match !prop_pool with Some l -> l | _ -> assert false)
;;
-(* automatically performes the union of a given list of patterns *)
-let rec pattern_list_ex = function
- | [] -> []
- | [(apreamble, apattern, afragid)] -> pattern_ex (apreamble, apattern, afragid)
- | (apreamble, apattern, afragid) :: tail ->
- union_ex (pattern_ex (apreamble, apattern, afragid)) (pattern_list_ex tail)
-
(* execute_ex env q *)
(* [env] is the attributed uri environment in which the query [q] *)
(* must be evaluated *)
use_ex (execute_ex env alist) asvar (get_prop_id "refObj") (* "F" (*"refObj"*) *)
| MQUse (alist, asvar) ->
use_ex (execute_ex env alist) asvar (get_prop_id "backPointer") (* "B" (*"backPointer"*) *)
- | MQPattern l ->
- pattern_list_ex l
+ | MQPattern (apreamble, apattern, afragid) ->
+ pattern_ex (apreamble, apattern, afragid)
| MQUnion (l1, l2) ->
union_ex (execute_ex env l1) (execute_ex env l2)
| MQDiff (l1, l2) ->
in
let ul1 = set_of_result (None,!execute env q1) in
let ul2 = set_of_result (None,!execute env q2) in
-prerr_endline ("MQSETEQUAL(" ^ string_of_int (List.length (!execute env q1)) ^ ">" ^ string_of_int (List.length ul1) ^ "," ^ string_of_int (List.length (!execute env q2)) ^ ">" ^ string_of_int (List.length ul2) ^ ")") ; flush stderr ;
+ print_endline ("MQSETEQUAL(" ^
+ string_of_int (List.length (!execute env q1)) ^ ">" ^
+ string_of_int (List.length ul1) ^ "," ^
+ string_of_int (List.length (!execute env q2)) ^ ">" ^
+ string_of_int (List.length ul2) ^ ")") ;
+ flush stdout ;
(try
List.fold_left2 (fun b uri1 uri2 -> b && uri1=uri2) true ul1 ul2
with
in
let ul1 = set_of_result (None,!execute env q1) in
let ul2 = set_of_result (None,!execute env q2) in
-prerr_endline ("MQSUBSET(" ^ string_of_int (List.length (!execute env q1)) ^ ">" ^ string_of_int (List.length ul1) ^ "," ^ string_of_int (List.length (!execute env q2)) ^ ">" ^ string_of_int (List.length ul2) ^ ")") ; flush stderr ;
+ print_endline ("MQSUBSET(" ^
+ string_of_int (List.length (!execute env q1)) ^ ">" ^
+ string_of_int (List.length ul1) ^ "," ^
+ string_of_int (List.length (!execute env q2)) ^ ">" ^
+ string_of_int (List.length ul2) ^ ")") ;
+ flush stdout ;
let rec is_subset s1 s2 =
match s1,s2 with
[],_ -> true
let after = Unix.time ()
and ll1 = string_of_int (List.length alist) in
let diff = string_of_float (after -. before) in
- prerr_endline
+ print_endline
("SORTEDBY(" ^ ll1 ^ ") = " ^ string_of_int (List.length res) ^
": " ^ diff ^ "s") ;
- flush stderr ;
+ flush stdout ;
res
;;
let ll1 = string_of_int (List.length l1) in
let ll2 = string_of_int (List.length l2) in
let diff = string_of_float (after -. before) in
- prerr_endline ("UNION(" ^ ll1 ^ "," ^ ll2 ^ "): " ^ diff ^ "s") ;
- flush stderr ;
+ print_endline ("UNION(" ^ ll1 ^ "," ^ ll2 ^ "): " ^ diff ^ "s") ;
+ flush stdout ;
res
;;
projects / helm.git / commitdiff