--- /dev/null
+(* Copyright (C) 2005, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+
+(* $Id: termAcicContent.ml 9304 2008-12-05 23:12:39Z sacerdot $ *)
+
+open Printf
+
+module Ast = CicNotationPt
+
+let debug = false
+let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
+
+(*
+type interpretation_id = int
+
+let idref id t = Ast.AttributedTerm (`IdRef id, t)
+
+type term_info =
+ { sort: (Cic.id, Ast.sort_kind) Hashtbl.t;
+ uri: (Cic.id, UriManager.uri) Hashtbl.t;
+ }
+
+let get_types uri =
+ let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
+ match o with
+ | Cic.InductiveDefinition (l,_,lpsno,_) -> l, lpsno
+ | _ -> assert false
+
+let name_of_inductive_type uri i =
+ let types, _ = get_types uri in
+ let (name, _, _, _) = try List.nth types i with Not_found -> assert false in
+ name
+
+ (* returns <name, type> pairs *)
+let constructors_of_inductive_type uri i =
+ let types, _ = get_types uri in
+ let (_, _, _, constructors) =
+ try List.nth types i with Not_found -> assert false
+ in
+ constructors
+
+ (* returns name only *)
+let constructor_of_inductive_type uri i j =
+ (try
+ fst (List.nth (constructors_of_inductive_type uri i) (j-1))
+ with Not_found -> assert false)
+
+ (* returns the number of left parameters *)
+let left_params_no_of_inductive_type uri =
+ snd (get_types uri)
+*)
+
+(* CODICE c&p da NCicPp *)
+let r2s pp_fix_name r =
+ try
+ match r with
+ | NReference.Ref (u,NReference.Ind (_,i,_)) ->
+ (match NCicLibrary.get_obj u with
+ | _,_,_,_, NCic.Inductive (_,_,itl,_) ->
+ let _,name,_,_ = List.nth itl i in name
+ | _ -> assert false)
+ | NReference.Ref (u,NReference.Con (i,j,_)) ->
+ (match NCicLibrary.get_obj u with
+ | _,_,_,_, NCic.Inductive (_,_,itl,_) ->
+ let _,_,_,cl = List.nth itl i in
+ let _,name,_ = List.nth cl (j-1) in name
+ | _ -> assert false)
+ | NReference.Ref (u,(NReference.Decl | NReference.Def _)) ->
+ (match NCicLibrary.get_obj u with
+ | _,_,_,_, NCic.Constant (_,name,_,_,_) -> name
+ | _ -> assert false)
+ | NReference.Ref (u,(NReference.Fix (i,_,_)|NReference.CoFix i)) ->
+ (match NCicLibrary.get_obj u with
+ | _,_,_,_, NCic.Fixpoint (_,fl,_) ->
+ if pp_fix_name then
+ let _,name,_,_,_ = List.nth fl i in name
+ else
+ NUri.name_of_uri u ^"("^ string_of_int i ^ ")"
+ | _ -> assert false)
+ with NCicLibrary.ObjectNotFound _ -> NReference.string_of_reference r
+;;
+
+let nast_of_cic =
+ let rec k = function
+ | NCic.Rel n -> Ast.Ident (string_of_int n, None)
+ | NCic.Const r -> Ast.Ident (r2s true r, None)
+ | NCic.Meta (n,l) -> Ast.Meta (n, [](*aux_context l*))
+ | NCic.Sort NCic.Prop -> Ast.Sort `Prop
+ | NCic.Sort NCic.Type _ -> Ast.Sort `Set
+ | NCic.Implicit `Hole -> Ast.UserInput
+ | NCic.Implicit _ -> Ast.Implicit
+ | NCic.Prod (n,s,t) ->
+ let binder_kind = `Forall in
+ Ast.Binder (binder_kind, (Ast.Ident (n,None), Some (k s)), k t)
+ | NCic.Lambda (n,s,t) ->
+ Ast.Binder (`Lambda,(Ast.Ident (n,None), Some (k s)), k t)
+ | NCic.LetIn (n,s,ty,t) ->
+ Ast.LetIn ((Ast.Ident (n,None), Some (k ty)), k s, k t)
+ | NCic.Appl args -> Ast.Appl (List.map k args)
+ (*| NCic.AConst (id,uri,substs) ->
+ register_uri id uri;
+ idref id (Ast.Ident (UriManager.name_of_uri uri, aux_substs substs))*)
+ | NCic.Match (uri,ty,te,patterns) ->
+(*
+ let name = NReference.name_of_reference uri in
+ let uri_str = UriManager.string_of_uri uri in
+ let puri_str = sprintf "%s#xpointer(1/%d)" uri_str (typeno+1) in
+ let ctor_puri j =
+ UriManager.uri_of_string
+ (sprintf "%s#xpointer(1/%d/%d)" uri_str (typeno+1) j)
+ in
+ let case_indty = name, Some (UriManager.uri_of_string puri_str) in
+ let constructors = constructors_of_inductive_type uri typeno in
+ let lpsno = left_params_no_of_inductive_type uri in
+ let rec eat_branch n ty pat =
+ match (ty, pat) with
+ | NCic.Prod (_, _, t), _ when n > 0 -> eat_branch (pred n) t pat
+ | NCic.Prod (_, _, t), NCic.ALambda (_, name, s, t') ->
+ let (cv, rhs) = eat_branch 0 t t' in
+ (CicNotationUtil.name_of_cic_name name, Some (k s)) :: cv, rhs
+ | _, _ -> [], k pat
+ in
+ let j = ref 0 in
+ let patterns =
+ try
+ List.map2
+ (fun (name, ty) pat ->
+ incr j;
+ let name,(capture_variables,rhs) =
+ match output_type with
+ `Term -> name, eat_branch lpsno ty pat
+ | `Pattern -> "_", ([], k pat)
+ in
+ Ast.Pattern (name, Some (ctor_puri !j), capture_variables), rhs
+ ) constructors patterns
+ with Invalid_argument _ -> assert false
+ in
+ let indty =
+ match output_type with
+ `Pattern -> None
+ | `Term -> Some case_indty
+ in
+ idref id (Ast.Case (k te, indty, Some (k ty), patterns))
+*) Ast.Ident ("Un case",None)
+ in
+ k
+;;
+
+let map_sequent (i,(n,context,ty):int * NCic.conjecture) =
+ let module K = Content in
+ let context' =
+ List.map
+ (function
+ | name,NCic.Decl t ->
+ Some
+ (* We should call build_decl_item, but we have not computed *)
+ (* the inner-types ==> we always produce a declaration *)
+ (`Declaration
+ { K.dec_name = (Some name);
+ K.dec_id = "-1";
+ K.dec_inductive = false;
+ K.dec_aref = "-1";
+ K.dec_type = t
+ })
+ | name,NCic.Def (t,ty) ->
+ Some
+ (* We should call build_def_item, but we have not computed *)
+ (* the inner-types ==> we always produce a declaration *)
+ (`Definition
+ { K.def_name = (Some name);
+ K.def_id = "-1";
+ K.def_aref = "-1";
+ K.def_term = t;
+ K.def_type = ty
+ })
+ ) context
+ in
+ "-1",i,context',ty
+;;
+
+(*
+ (* persistent state *)
+
+let initial_level2_patterns32 () = Hashtbl.create 211
+let initial_interpretations () = Hashtbl.create 211
+
+let level2_patterns32 = ref (initial_level2_patterns32 ())
+(* symb -> id list ref *)
+let interpretations = ref (initial_interpretations ())
+let compiled32 = ref None
+let pattern32_matrix = ref []
+let counter = ref ~-1
+
+let stack = ref []
+
+let push () =
+ stack := (!counter,!level2_patterns32,!interpretations,!compiled32,!pattern32_matrix)::!stack;
+ counter := ~-1;
+ level2_patterns32 := initial_level2_patterns32 ();
+ interpretations := initial_interpretations ();
+ compiled32 := None;
+ pattern32_matrix := []
+;;
+
+let pop () =
+ match !stack with
+ [] -> assert false
+ | (ocounter,olevel2_patterns32,ointerpretations,ocompiled32,opattern32_matrix)::old ->
+ stack := old;
+ counter := ocounter;
+ level2_patterns32 := olevel2_patterns32;
+ interpretations := ointerpretations;
+ compiled32 := ocompiled32;
+ pattern32_matrix := opattern32_matrix
+;;
+
+let get_compiled32 () =
+ match !compiled32 with
+ | None -> assert false
+ | Some f -> Lazy.force f
+
+let set_compiled32 f = compiled32 := Some f
+
+let add_idrefs =
+ List.fold_right (fun idref t -> Ast.AttributedTerm (`IdRef idref, t))
+
+let instantiate32 term_info idrefs env symbol args =
+ let rec instantiate_arg = function
+ | Ast.IdentArg (n, name) ->
+ let t =
+ try List.assoc name env
+ with Not_found -> prerr_endline ("name not found in env: "^name);
+ assert false
+ in
+ let rec count_lambda = function
+ | Ast.AttributedTerm (_, t) -> count_lambda t
+ | Ast.Binder (`Lambda, _, body) -> 1 + count_lambda body
+ | _ -> 0
+ in
+ let rec add_lambda t n =
+ if n > 0 then
+ let name = CicNotationUtil.fresh_name () in
+ Ast.Binder (`Lambda, (Ast.Ident (name, None), None),
+ Ast.Appl [add_lambda t (n - 1); Ast.Ident (name, None)])
+ else
+ t
+ in
+ add_lambda t (n - count_lambda t)
+ in
+ let head =
+ let symbol = Ast.Symbol (symbol, 0) in
+ add_idrefs idrefs symbol
+ in
+ if args = [] then head
+ else Ast.Appl (head :: List.map instantiate_arg args)
+
+let rec ast_of_acic1 ~output_type term_info annterm =
+ let id_to_uris = term_info.uri in
+ let register_uri id uri = Hashtbl.add id_to_uris id uri in
+ match (get_compiled32 ()) annterm with
+ | None ->
+ ast_of_acic0 ~output_type term_info annterm (ast_of_acic1 ~output_type)
+ | Some (env, ctors, pid) ->
+ let idrefs =
+ List.map
+ (fun annterm ->
+ let idref = CicUtil.id_of_annterm annterm in
+ (try
+ register_uri idref
+ (CicUtil.uri_of_term (Deannotate.deannotate_term annterm))
+ with Invalid_argument _ -> ());
+ idref)
+ ctors
+ in
+ let env' =
+ List.map
+ (fun (name, term) -> name, ast_of_acic1 ~output_type term_info term) env
+ in
+ let _, symbol, args, _ =
+ try
+ Hashtbl.find !level2_patterns32 pid
+ with Not_found -> assert false
+ in
+ let ast = instantiate32 term_info idrefs env' symbol args in
+ Ast.AttributedTerm (`IdRef (CicUtil.id_of_annterm annterm), ast)
+
+let load_patterns32 t =
+ let t =
+ HExtlib.filter_map (function (true, ap, id) -> Some (ap, id) | _ -> None) t
+ in
+ set_compiled32 (lazy (Acic2astMatcher.Matcher32.compiler t))
+
+let ast_of_acic ~output_type id_to_sort annterm =
+ debug_print (lazy ("ast_of_acic <- "
+ ^ CicPp.ppterm (Deannotate.deannotate_term annterm)));
+ let term_info = { sort = id_to_sort; uri = Hashtbl.create 211 } in
+ let ast = ast_of_acic1 ~output_type term_info annterm in
+ debug_print (lazy ("ast_of_acic -> " ^ CicNotationPp.pp_term ast));
+ ast, term_info.uri
+
+let fresh_id =
+ fun () ->
+ incr counter;
+ !counter
+
+let add_interpretation dsc (symbol, args) appl_pattern =
+ let id = fresh_id () in
+ Hashtbl.add !level2_patterns32 id (dsc, symbol, args, appl_pattern);
+ pattern32_matrix := (true, appl_pattern, id) :: !pattern32_matrix;
+ load_patterns32 !pattern32_matrix;
+ (try
+ let ids = Hashtbl.find !interpretations symbol in
+ ids := id :: !ids
+ with Not_found -> Hashtbl.add !interpretations symbol (ref [id]));
+ id
+
+let get_all_interpretations () =
+ List.map
+ (function (_, _, id) ->
+ let (dsc, _, _, _) =
+ try
+ Hashtbl.find !level2_patterns32 id
+ with Not_found -> assert false
+ in
+ (id, dsc))
+ !pattern32_matrix
+
+let get_active_interpretations () =
+ HExtlib.filter_map (function (true, _, id) -> Some id | _ -> None)
+ !pattern32_matrix
+
+let set_active_interpretations ids =
+ let pattern32_matrix' =
+ List.map
+ (function
+ | (_, ap, id) when List.mem id ids -> (true, ap, id)
+ | (_, ap, id) -> (false, ap, id))
+ !pattern32_matrix
+ in
+ pattern32_matrix := pattern32_matrix';
+ load_patterns32 !pattern32_matrix
+
+exception Interpretation_not_found
+
+let lookup_interpretations symbol =
+ try
+ HExtlib.list_uniq
+ (List.sort Pervasives.compare
+ (List.map
+ (fun id ->
+ let (dsc, _, args, appl_pattern) =
+ try
+ Hashtbl.find !level2_patterns32 id
+ with Not_found -> assert false
+ in
+ dsc, args, appl_pattern)
+ !(Hashtbl.find !interpretations symbol)))
+ with Not_found -> raise Interpretation_not_found
+
+let remove_interpretation id =
+ (try
+ let dsc, symbol, _, _ = Hashtbl.find !level2_patterns32 id in
+ let ids = Hashtbl.find !interpretations symbol in
+ ids := List.filter ((<>) id) !ids;
+ Hashtbl.remove !level2_patterns32 id;
+ with Not_found -> raise Interpretation_not_found);
+ pattern32_matrix :=
+ List.filter (fun (_, _, id') -> id <> id') !pattern32_matrix;
+ load_patterns32 !pattern32_matrix
+
+let _ = load_patterns32 []
+
+let instantiate_appl_pattern
+ ~mk_appl ~mk_implicit ~term_of_uri env appl_pattern
+=
+ let lookup name =
+ try List.assoc name env
+ with Not_found ->
+ prerr_endline (sprintf "Name %s not found" name);
+ assert false
+ in
+ let rec aux = function
+ | Ast.UriPattern uri -> term_of_uri uri
+ | Ast.ImplicitPattern -> mk_implicit false
+ | Ast.VarPattern name -> lookup name
+ | Ast.ApplPattern terms -> mk_appl (List.map aux terms)
+ in
+ aux appl_pattern
+*)
end;
self#load_root ~root:mathml#get_documentElement
+ method nload_sequent metasenv subst metano =
+ let sequent = List.assoc metano metasenv in
+ let mathml =
+ ApplyTransformation.nmml_of_cic_sequent metasenv subst (metano,sequent)
+ in
+ if BuildTimeConf.debug then begin
+ let name =
+ "/tmp/sequent_viewer_" ^ string_of_int (Unix.getuid ()) ^ ".xml" in
+ HLog.debug ("load_sequent: dumping MathML to ./" ^ name);
+ ignore (domImpl#saveDocumentToFile ~name ~doc:mathml ())
+ end;
+ self#load_root ~root:mathml#get_documentElement
+
method load_object obj =
let use_diff = false in (* ZACK TODO use XmlDiff when re-rendering? *)
let (mathml,
val mutable page2goal = [] (* associative list: page no -> goal no *)
val mutable goal2page = [] (* the other way round *)
val mutable goal2win = [] (* associative list: goal no -> scrolled win *)
- val mutable _metasenv = []
+ val mutable _metasenv = `Old []
val mutable scrolledWin: GBin.scrolled_window option = None
(* scrolled window to which the sequentViewer is currently attached *)
val logo = (GMisc.image
page2goal <- [];
goal2page <- [];
goal2win <- [];
- _metasenv <- [];
+ _metasenv <- `Old [];
self#script#setGoal None
method load_sequents
{ proof = (_,metasenv,_subst,_,_, _) as proof; stack = stack }
=
- _metasenv <- metasenv;
+ _metasenv <- `Old metasenv;
pages <- 0;
let win goal_switch =
let w =
self#script#setGoal (Some (goal_of_switch goal_switch));
self#render_page ~page ~goal_switch))
+ method nload_sequents
+ { NTacStatus.istatus = { NTacStatus.pstatus = (_,_,metasenv,subst,_) }; gstatus = stack }
+ =
+ _metasenv <- `New (metasenv,subst);
+ pages <- 0;
+ let win goal_switch =
+ let w =
+ GBin.scrolled_window ~hpolicy:`AUTOMATIC ~vpolicy:`ALWAYS
+ ~shadow_type:`IN ~show:true ()
+ in
+ let reparent () =
+ scrolledWin <- Some w;
+ match cicMathView#misc#parent with
+ | None -> w#add cicMathView#coerce
+ | Some parent ->
+ let parent =
+ match cicMathView#misc#parent with
+ None -> assert false
+ | Some p -> GContainer.cast_container p
+ in
+ parent#remove cicMathView#coerce;
+ w#add cicMathView#coerce
+ in
+ goal2win <- (goal_switch, reparent) :: goal2win;
+ w#coerce
+ in
+ assert (
+ let stack_goals = Stack.open_goals stack in
+ let proof_goals = List.map fst metasenv in
+ if
+ HExtlib.list_uniq (List.sort Pervasives.compare stack_goals)
+ <> List.sort Pervasives.compare proof_goals
+ then begin
+ prerr_endline ("STACK GOALS = " ^ String.concat " " (List.map string_of_int stack_goals));
+ prerr_endline ("PROOF GOALS = " ^ String.concat " " (List.map string_of_int proof_goals));
+ false
+ end
+ else true
+ );
+ let render_switch =
+ function Stack.Open i ->`Meta i | Stack.Closed i ->`Closed (`Meta i)
+ in
+ let page = ref 0 in
+ let added_goals = ref [] in
+ (* goals can be duplicated on the tack due to focus, but we should avoid
+ * multiple labels in the user interface *)
+ let add_tab markup goal_switch =
+ let goal = Stack.goal_of_switch goal_switch in
+ if not (List.mem goal !added_goals) then begin
+ ignore(notebook#append_page
+ ~tab_label:(tab_label markup) (win goal_switch));
+ page2goal <- (!page, goal_switch) :: page2goal;
+ goal2page <- (goal_switch, !page) :: goal2page;
+ incr page;
+ pages <- pages + 1;
+ added_goals := goal :: !added_goals
+ end
+ in
+ let add_switch _ _ (_, sw) = add_tab (render_switch sw) sw in
+ Stack.iter (** populate notebook with tabs *)
+ ~env:(fun depth tag (pos, sw) ->
+ let markup =
+ match depth, pos with
+ | 0, 0 -> `Current (render_switch sw)
+ | 0, _ -> `Shift (pos, `Current (render_switch sw))
+ | 1, pos when Stack.head_tag stack = `BranchTag ->
+ `Shift (pos, render_switch sw)
+ | _ -> render_switch sw
+ in
+ add_tab markup sw)
+ ~cont:add_switch ~todo:add_switch
+ stack;
+ switch_page_callback <-
+ Some (notebook#connect#switch_page ~callback:(fun page ->
+ let goal_switch =
+ try List.assoc page page2goal with Not_found -> assert false
+ in
+ self#script#setGoal (Some (goal_of_switch goal_switch));
+ self#render_page ~page ~goal_switch))
+
method private render_page ~page ~goal_switch =
(match goal_switch with
- | Stack.Open goal -> cicMathView#load_sequent _metasenv goal
+ | Stack.Open goal ->
+ (match _metasenv with
+ `Old menv -> cicMathView#load_sequent menv goal
+ | `New (menv,subst) -> cicMathView#nload_sequent menv subst goal)
| Stack.Closed goal ->
let doc = Lazy.force closed_goal_mathml in
cicMathView#load_root ~root:doc#get_documentElement);
projects / helm.git / commitdiff