-requires="helm-library helm-acic_content helm-ng_kernel"
+requires="helm-library helm-acic_content helm-ng_refiner"
version="0.0.1"
archive(byte)="ng_cic_content.cma"
archive(native)="ng_cic_content.cmxa"
ng_kernel \
acic_content \
grafite \
+ ng_refiner \
ng_cic_content \
content_pres \
cic_unification \
disambiguation \
cic_disambiguation \
lexicon \
- ng_refiner \
ng_disambiguation \
grafite_parser \
ng_paramodulation \
try HExtlib.split_nth (cpos+sats+1) tl with Failure _ -> [],[]
in
if rest = [] then
- idref aid (List.nth (List.map k tl) cpos)
+ idref aid (k (List.nth tl cpos))
else
idref aid (Ast.Appl (List.map k (List.nth tl cpos::rest)))
else
- idref aid (Ast.Appl (List.map k tl))
+ idref aid (Ast.Appl (List.map k args))
else
idref aid (Ast.Appl (List.map k args)))
| Cic.AAppl (aid,args) ->
gallina8Parser.cmi: types.cmo
grafiteParser.cmi: types.cmo
grafite.cmi: types.cmo
+engine.cmi:
+types.cmo:
+types.cmx:
+options.cmo:
+options.cmx:
gallina8Parser.cmo: types.cmo options.cmo gallina8Parser.cmi
gallina8Parser.cmx: types.cmx options.cmx gallina8Parser.cmi
gallina8Lexer.cmo: options.cmo gallina8Parser.cmi
type t
val iter : t -> (constant_name path -> dataset -> unit) -> unit
+ val fold : t -> (constant_name path -> dataset -> 'b -> 'b) -> 'b -> 'b
val empty : t
val index : t -> input -> data -> t
let iter dt f = DiscriminationTree.iter (fun p x -> f p x) dt;;
+ let fold dt f = DiscriminationTree.fold (fun p x -> f p x) dt;;
+
let index tree term info =
let ps = I.path_string_of term in
let ps_set =
type t
val iter : t -> (constant_name path -> dataset -> unit) -> unit
+ val fold : t -> (constant_name path -> dataset -> 'b -> 'b) -> 'b -> 'b
val empty : t
val index : t -> input -> data -> t
The second one can be shorter and is padded with a default value.
This function cannot fail. *)
val list_iter_default2: ('a -> 'b -> unit) -> 'a list -> 'b -> 'b list -> unit
+exception FailureAt of int
(* Checks a predicate in parallel on three lists, the first two having the same
length (otherwise it raises Invalid_argument). It stops when the first two
- lists are empty. The third one can be shorter and is padded with a default value. *)
+ lists are empty. The third one can be shorter and is padded with a default
+ value. It can also raise FailureAt when ??? *)
val list_forall_default3: ('a -> 'b -> 'c -> bool) -> 'a list -> 'b list -> 'c -> 'c list -> bool
val list_forall_default3_var: ('a -> 'b -> 'c -> bool) -> 'a list -> 'b list -> 'c -> 'c list -> bool
-exception FailureAt of int
-
(** split_nth n l
* @returns two list, the first contains at least n elements, the second the
* remaining ones
;;
(* CODICE c&p da NCicPp *)
-let nast_of_cic0
+let nast_of_cic0 status
~(idref:
?reference:NReference.reference -> CicNotationPt.term -> CicNotationPt.term)
- ~output_type ~subst k ~context =
+ ~output_type ~metasenv ~subst k ~context =
function
| NCic.Rel n ->
(try
(match hd with
| NCic.Appl l -> NCic.Appl (l@args)
| _ -> NCic.Appl (hd :: args)))
- | NCic.Appl args -> idref (Ast.Appl (List.map (k ~context) args))
+ | NCic.Appl args as t ->
+ let args =
+ if not !Acic2content.hide_coercions then args
+ else
+ match
+ NCicCoercion.match_coercion status ~metasenv ~context ~subst t
+ with
+ | None -> args
+ | Some (_,sats,cpos) ->
+(* CSC: sats e' il numero di pi, ma non so cosa farmene! voglio il numero di
+ argomenti da saltare, come prima! *)
+ if cpos < List.length args - 1 then
+ List.nth args (cpos + 1) ::
+ try snd (HExtlib.split_nth (cpos+sats+2) args) with Failure _->[]
+ else
+ args
+ in
+ (match args with
+ [arg] -> idref (k ~context arg)
+ | _ -> idref (Ast.Appl (List.map (k ~context) args)))
| NCic.Match (NReference.Ref (uri,_) as r,outty,te,patterns) ->
let name = NUri.name_of_uri uri in
(* CSC
if args = [] then head
else Ast.Appl (head :: List.map instantiate_arg args)
-let rec nast_of_cic1 ~idref ~output_type ~subst ~context term =
+let rec nast_of_cic1 status ~idref ~output_type ~metasenv ~subst ~context term =
match (get_compiled32 ()) term with
| None ->
- nast_of_cic0 ~idref ~output_type ~subst
- (nast_of_cic1 ~idref ~output_type ~subst) ~context term
+ nast_of_cic0 status ~idref ~output_type ~metasenv ~subst
+ (nast_of_cic1 status ~idref ~output_type ~metasenv ~subst) ~context term
| Some (env, ctors, pid) ->
let idrefs =
List.map
List.map
(fun (name, term) ->
name,
- nast_of_cic1 ~idref ~output_type ~subst ~context term
+ nast_of_cic1 status ~idref ~output_type ~subst ~metasenv ~context
+ term
) env
in
let _, symbol, args, _ =
aux appl_pattern
*)
-let nmap_sequent0 ~idref ~subst (i,(n,context,ty):int * NCic.conjecture) =
+let nmap_sequent0 status ~idref ~metasenv ~subst (i,(n,context,ty)) =
let module K = Content in
- let nast_of_cic = nast_of_cic1 ~idref ~output_type:`Term ~subst in
+ let nast_of_cic =
+ nast_of_cic1 status ~idref ~output_type:`Term ~metasenv ~subst in
let context',_ =
List.fold_right
(fun item (res,context) ->
("-1",i,context',nast_of_cic ~context ty)
;;
-let nmap_sequent ~subst metasenv =
+let nmap_sequent status ~metasenv ~subst conjecture =
let module K = Content in
let ids_to_refs = Hashtbl.create 211 in
let register_ref = Hashtbl.add ids_to_refs in
- nmap_sequent0 ~idref:(idref register_ref) ~subst metasenv, ids_to_refs
+ nmap_sequent0 status ~idref:(idref register_ref) ~metasenv ~subst conjecture,
+ ids_to_refs
;;
let object_prefix = "obj:";;
}
;;
-let nmap_obj (uri,_,metasenv,subst,kind) =
+let nmap_obj status (uri,_,metasenv,subst,kind) =
let module K = Content in
let ids_to_refs = Hashtbl.create 211 in
let register_ref = Hashtbl.add ids_to_refs in
let idref = idref register_ref in
let nast_of_cic =
- nast_of_cic1 ~idref ~output_type:`Term ~subst in
+ nast_of_cic1 status ~idref ~output_type:`Term ~metasenv ~subst in
let seed = ref 0 in
let conjectures =
match metasenv with
[] -> None
| _ -> (*Some (List.map (map_conjectures seed) metasenv)*)
(*CSC: used to be the previous line, that uses seed *)
- Some (List.map (nmap_sequent0 ~idref ~subst) metasenv)
+ Some (List.map (nmap_sequent0 status ~idref ~metasenv ~subst) metasenv)
in
let res =
match kind with
type id = string
val nmap_sequent:
- subst:NCic.substitution -> int * NCic.conjecture ->
- CicNotationPt.term Content.conjecture *
- (id, NReference.reference) Hashtbl.t (* id -> reference *)
+ #NCicCoercion.status -> metasenv:NCic.metasenv -> subst:NCic.substitution ->
+ int * NCic.conjecture ->
+ CicNotationPt.term Content.conjecture *
+ (id, NReference.reference) Hashtbl.t (* id -> reference *)
val nmap_obj:
- NCic.obj ->
+ #NCicCoercion.status -> NCic.obj ->
CicNotationPt.term Content.cobj *
(id, NReference.reference) Hashtbl.t (* id -> reference *)
metasenv, NCicUntrusted.mk_appl t args, ty, List.nth args arg)
(CoercionSet.elements candidates)
;;
+
+(* CSC: very inefficient implementation!
+ Enrico, can we use a discrimination tree here? *)
+let match_coercion status ~metasenv ~subst ~context t =
+ let db =
+ DB.fold (fst (status#coerc_db)) (fun _ v l -> (CoercionSet.elements v)@l) []
+ in
+ try
+ Some
+ (List.find
+ (fun (p,_,_) ->
+ try
+ let t =
+ match p,t with
+ NCic.Appl lp, NCic.Appl lt ->
+ (match fst (HExtlib.split_nth (List.length lp) lt) with
+ [t] -> t
+ | l -> NCic.Appl l)
+ | _,NCic.Appl (he::_) -> he
+ | _,_ -> t
+ in
+ NCicReduction.alpha_eq metasenv subst context p t
+ with
+ Failure _ -> false (* raised by split_nth *)
+ ) db)
+ with
+ Not_found -> None
+;;
(* enriched metasenv, new term, its type, metavriable to
* be unified with the old term *)
(NCic.metasenv * NCic.term * NCic.term * NCic.term) list
+
+(* returns (coercion,arity,arg) *)
+val match_coercion:
+ #status -> metasenv:NCic.metasenv -> subst:NCic.substitution ->
+ context:NCic.context -> NCic.term -> (NCic.term * int * int) option
(asequent,
(ids_to_terms,ids_to_father_ids,ids_to_hypotheses,ids_to_inner_sorts)))
-let nmml_of_cic_sequent metasenv subst sequent =
+let nmml_of_cic_sequent status metasenv subst sequent =
let content_sequent,ids_to_refs =
- NTermCicContent.nmap_sequent ~subst sequent in
+ NTermCicContent.nmap_sequent status ~metasenv ~subst sequent in
let pres_sequent =
Sequent2pres.nsequent2pres ids_to_refs subst content_sequent in
let xmlpres = mpres_document pres_sequent in
(ids_to_terms, ids_to_father_ids, ids_to_conjectures, ids_to_hypotheses,
ids_to_inner_sorts,ids_to_inner_types)))
-let nmml_of_cic_object obj =
- let cobj,ids_to_nrefs = NTermCicContent.nmap_obj obj in
+let nmml_of_cic_object status obj =
+ let cobj,ids_to_nrefs = NTermCicContent.nmap_obj status obj in
let pres_sequent = Content2pres.ncontent2pres ~ids_to_nrefs cobj in
let xmlpres = mpres_document pres_sequent in
Xml2Gdome.document_of_xml DomMisc.domImpl xmlpres
(Cic.id, Cic2acic.sort_kind) Hashtbl.t)) (* ids_to_inner_sorts *)
val nmml_of_cic_sequent:
+ #NCicCoercion.status ->
NCic.metasenv -> NCic.substitution -> (* metasenv, substitution *)
int * NCic.conjecture -> (* sequent *)
Gdome.document (* Math ML *)
(Cic.id, Cic2acic.sort_kind) Hashtbl.t * (* ids_to_inner_sorts *)
(Cic.id, Cic2acic.anntypes) Hashtbl.t)) (* ids_to_inner_types *)
-val nmml_of_cic_object: NCic.obj -> Gdome.document
+val nmml_of_cic_object: #NCicCoercion.status -> NCic.obj -> Gdome.document
val txt_of_cic_term:
map_unicode_to_tex:bool -> int -> Cic.metasenv -> Cic.context -> Cic.term ->
sequents_viewer#reset;
match grafite_status#proof_status with
| Incomplete_proof ({ stack = stack } as incomplete_proof) ->
- sequents_viewer#load_sequents incomplete_proof;
+ sequents_viewer#load_sequents grafite_status incomplete_proof;
(try
script#setGoal (Some (Continuationals.Stack.find_goal stack));
let goal =
None -> assert false
| Some n -> n
in
- sequents_viewer#goto_sequent goal
+ sequents_viewer#goto_sequent grafite_status goal
with Failure _ -> script#setGoal None);
| Proof proof -> sequents_viewer#load_logo_with_qed
| No_proof ->
None -> assert false
| Some n -> n
in
- sequents_viewer#goto_sequent goal
+ sequents_viewer#goto_sequent grafite_status goal
with Failure _ -> script#setGoal None);
| `CommandMode -> sequents_viewer#load_logo
)
(** load a sequent and render it into parent widget *)
method load_sequent: Cic.metasenv -> int -> unit
- method nload_sequent: NCic.metasenv -> NCic.substitution -> int -> unit
+ method nload_sequent:
+ #NCicCoercion.status -> NCic.metasenv -> NCic.substitution -> int -> unit
method load_object: Cic.obj -> unit
- method load_nobject: NCic.obj -> unit
+ method load_nobject: #NCicCoercion.status -> NCic.obj -> unit
end
class type sequentsViewer =
method reset: unit
method load_logo: unit
method load_logo_with_qed: unit
- method load_sequents: GrafiteTypes.incomplete_proof -> unit
+ method load_sequents:
+ #NCicCoercion.status -> GrafiteTypes.incomplete_proof -> unit
method nload_sequents: #NTacStatus.tac_status -> unit
- method goto_sequent: int -> unit (* to be called _after_ load_sequents *)
+ method goto_sequent:
+ #NCicCoercion.status -> int -> unit (* to be called _after_ load_sequents *)
method cicMathView: cicMathView
end
end;
self#load_root ~root:mathml#get_documentElement
- method nload_sequent metasenv subst metano =
+ method nload_sequent:
+ 'status. #NCicCoercion.status as 'status -> NCic.metasenv ->
+ NCic.substitution -> int -> unit
+ = fun status metasenv subst metano ->
let sequent = List.assoc metano metasenv in
let mathml =
- ApplyTransformation.nmml_of_cic_sequent metasenv subst (metano,sequent)
+ ApplyTransformation.nmml_of_cic_sequent status metasenv subst
+ (metano,sequent)
in
if BuildTimeConf.debug then begin
let name =
self#load_root ~root:mathml#get_documentElement;
current_mathml <- Some mathml);
- method load_nobject obj =
- let mathml = ApplyTransformation.nmml_of_cic_object obj in
+ method load_nobject :
+ 'status. #NCicCoercion.status as 'status -> NCic.obj -> unit
+ = fun status obj ->
+ let mathml = ApplyTransformation.nmml_of_cic_object status obj in
(*
self#set_cic_info
(Some (None, ids_to_terms, ids_to_hypotheses, ids_to_father_ids, ids_to_inner_types, Some annobj));
_metasenv <- `Old [];
self#script#setGoal None
- method load_sequents
- { proof = (_,metasenv,_subst,_,_, _) as proof; stack = stack }
- =
+ method load_sequents : 'status. #NCicCoercion.status as 'status -> 'a
+ = fun status { proof= (_,metasenv,_subst,_,_, _) as proof; stack = stack }
+ ->
_metasenv <- `Old metasenv;
pages <- 0;
let win 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))
+ self#render_page status ~page ~goal_switch))
method nload_sequents : 'status. #NTacStatus.tac_status as 'status -> unit
= fun status ->
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))
+ self#render_page status ~page ~goal_switch))
- method private render_page ~page ~goal_switch =
+ method private render_page:
+ 'status. #NCicCoercion.status as 'status -> page:int ->
+ goal_switch:Stack.switch -> unit
+ = fun status ~page ~goal_switch ->
(match goal_switch with
| Stack.Open goal ->
(match _metasenv with
`Old menv -> cicMathView#load_sequent menv goal
- | `New (menv,subst) -> cicMathView#nload_sequent menv subst goal)
+ | `New (menv,subst) ->
+ cicMathView#nload_sequent status menv subst goal)
| Stack.Closed goal ->
let doc = Lazy.force closed_goal_mathml in
cicMathView#load_root ~root:doc#get_documentElement);
List.assoc goal_switch goal2win ()
with Not_found -> assert false)
- method goto_sequent goal =
+ method goto_sequent: 'status. #NCicCoercion.status as 'status -> int -> unit
+ = fun status goal ->
let goal_switch, page =
try
List.find
with Not_found -> assert false
in
notebook#goto_page page;
- self#render_page page goal_switch
+ self#render_page status ~page ~goal_switch
end
self#_loadObj obj
| _ ->
match self#script#grafite_status#ng_mode with
- `ProofMode -> self#_loadNObj self#script#grafite_status#obj
+ `ProofMode ->
+ self#_loadNObj self#script#grafite_status
+ self#script#grafite_status#obj
| _ -> self#blank ()
(** loads a cic uri from the environment
method private _loadNReference (NReference.Ref (uri,_)) =
let obj = NCicEnvironment.get_checked_obj uri in
- self#_loadNObj obj
+ self#_loadNObj self#script#grafite_status obj
method private _loadUnivs uri =
let uri = UriManager.strip_xpointer uri in
self#_showMath;
mathView#load_object obj
- method private _loadNObj obj =
+ method private _loadNObj status obj =
(* showMath must be done _before_ loading the document, since if the
* widget is not mapped (hidden by the notebook) the document is not
* rendered *)
self#_showMath;
- mathView#load_nobject obj
+ mathView#load_nobject status obj
method private _loadTermCic term metasenv =
let context = self#script#proofContext in
∀A,B. ∀Ma: magma A. ∀Mb: magma B. magma_morphism ?? Ma Mb → magma B.
#A; #B; #Ma; #Mb; #f;
napply (mk_magma ???)
- [ napply (image ?? (mmcarr ?? (mmmcarr ???? f)) (mcarr ? Ma))
+ [ napply (image ?? (mmcarr ?? (mmmcarr ???? f)) Ma) (* NO COMPOSITE! *)
| #x; #y; nwhd in ⊢ (% → % → ?); *; #x0; *; #Hx0; #Hx1; *; #y0; *; #Hy0; #Hy1; nwhd;
napply (ex_intro ????)
[ napply (op ? x0 y0)
projects / helm.git / commitdiff