+disambiguatePp.cmi: disambiguateTypes.cmi
disambiguateChoices.cmi: disambiguateTypes.cmi
-cicTextualParser2.cmi: disambiguateTypes.cmi
disambiguate.cmi: disambiguateTypes.cmi
disambiguateTypes.cmo: disambiguateTypes.cmi
disambiguateTypes.cmx: disambiguateTypes.cmi
+disambiguatePp.cmo: disambiguateTypes.cmi disambiguatePp.cmi
+disambiguatePp.cmx: disambiguateTypes.cmx disambiguatePp.cmi
disambiguateChoices.cmo: disambiguateTypes.cmi disambiguateChoices.cmi
disambiguateChoices.cmx: disambiguateTypes.cmx disambiguateChoices.cmi
-cicTextualLexer2.cmo: cicTextualLexer2.cmi
-cicTextualLexer2.cmx: cicTextualLexer2.cmi
-cicTextualParser2.cmo: disambiguateTypes.cmi disambiguateChoices.cmi \
- cicTextualLexer2.cmi cicTextualParser2.cmi
-cicTextualParser2.cmx: disambiguateTypes.cmx disambiguateChoices.cmx \
- cicTextualLexer2.cmx cicTextualParser2.cmi
disambiguate.cmo: disambiguateTypes.cmi disambiguateChoices.cmi \
- cicTextualParser2.cmi disambiguate.cmi
+ disambiguate.cmi
disambiguate.cmx: disambiguateTypes.cmx disambiguateChoices.cmx \
- cicTextualParser2.cmx disambiguate.cmi
-logic_notation.cmo: disambiguateChoices.cmi cicTextualParser2.cmi
-logic_notation.cmx: disambiguateChoices.cmx cicTextualParser2.cmx
-arit_notation.cmo: disambiguateChoices.cmi cicTextualParser2.cmi
-arit_notation.cmx: disambiguateChoices.cmx cicTextualParser2.cmx
-tex_notation.cmo: cicTextualParser2.cmi
-tex_notation.cmx: cicTextualParser2.cmx
+ disambiguate.cmi
+arit_notation.cmo: disambiguateTypes.cmi disambiguateChoices.cmi
+arit_notation.cmx: disambiguateTypes.cmx disambiguateChoices.cmx
PACKAGE = cic_textual_parser2
REQUIRES = \
- helm-tactics helm-logger helm-cic_unification helm-cic_transformations \
+ helm-tactics helm-logger helm-cic_unification helm-cic_notation \
helm-utf8_macros \
ulex
-NOTATIONS = logic arit tex
-# NOTATIONS = logic arit
-INTERFACE_FILES = \
- disambiguateTypes.mli \
- disambiguateChoices.mli \
- cicTextualLexer2.mli \
- cicTextualParser2.mli \
+NOTATIONS = arit
+INTERFACE_FILES = \
+ disambiguateTypes.mli \
+ disambiguatePp.mli \
+ disambiguateChoices.mli \
disambiguate.mli
IMPLEMENTATION_FILES = \
$(patsubst %.mli, %.ml, $(INTERFACE_FILES)) \
$(patsubst %,%_notation.ml,$(NOTATIONS))
-all: test_lexer test_parser
-
-cicTextualLexer2.cmo: cicTextualLexer2.ml
- $(OCAMLC_P4) -c $<
-cicTextualParser2.cmo: cicTextualParser2.ml
- $(OCAMLC_P4) -c $<
-cicTextualLexer2.cmx: cicTextualLexer2.ml
- $(OCAMLOPT_P4) -c $<
-cicTextualParser2.cmx: cicTextualParser2.ml
- $(OCAMLOPT_P4) -c $<
-
-%_notation.cmo: %_notation.ml
- $(OCAMLC_P4) -c $<
-%_notation.cmx: %_notation.ml
- $(OCAMLOPT_P4) -c $<
-
-LOCAL_LINKOPTS = -package helm-cic_textual_parser2 -linkpkg
-test: test_lexer test_parser
-test_lexer: test_lexer.ml $(PACKAGE).cma
- $(OCAMLC) $(LOCAL_LINKOPTS) -o $@ $<
-test_parser: test_parser.ml $(PACKAGE).cma
- $(OCAMLC) $(LOCAL_LINKOPTS) -o $@ $<
+all:
clean: extra_clean
distclean: extra_clean
* http://helm.cs.unibo.it/
*)
-open CicTextualParser2
-
-EXTEND
- term: LEVEL "add"
- [
- [ t1 = term; SYMBOL "+"; t2 = term ->
- return_term loc (CicAst.Appl [CicAst.Symbol ("plus", 0); t1; t2])
- | t1 = term; SYMBOL "-"; t2 = term ->
- return_term loc (CicAst.Appl [CicAst.Symbol ("minus", 0); t1; t2])
- ]
- ];
- term: LEVEL "mult"
- [
- [ t1 = term; SYMBOL "*"; t2 = term ->
- return_term loc (CicAst.Appl [CicAst.Symbol ("times", 0); t1; t2])
- | t1 = term; SYMBOL "/"; t2 = term ->
- return_term loc (CicAst.Appl [CicAst.Symbol ("divide", 0); t1; t2])
- ]
- ];
- term: LEVEL "power"
- [
- [ t1 = term; SYMBOL "^"; t2 = term ->
- return_term loc (CicAst.Appl [CicAst.Symbol ("power", 0); t1; t2])
- ]
- ];
- term: LEVEL "inv"
- [
- [ SYMBOL "-"; t = term ->
- return_term loc (CicAst.Appl [CicAst.Symbol ("uminus", 0); t])
- ]
- ];
- term: LEVEL "relop"
- [
- [ t1 = term; SYMBOL <:unicode<leq>> (* ≤ *); t2 = term ->
- return_term loc (CicAst.Appl [CicAst.Symbol ("leq", 0); t1; t2])
- | t1 = term; SYMBOL <:unicode<geq>> (* ≥ *); t2 = term ->
- return_term loc (CicAst.Appl [CicAst.Symbol ("geq", 0); t1; t2])
- | t1 = term; SYMBOL "<"; t2 = term ->
- return_term loc (CicAst.Appl [CicAst.Symbol ("lt", 0); t1; t2])
- | t1 = term; SYMBOL ">"; t2 = term ->
- return_term loc (CicAst.Appl [CicAst.Symbol ("gt", 0); t1; t2])
- | t1 = term; SYMBOL <:unicode<ne>> (* ≠ *); t2 = term ->
- return_term loc (CicAst.Appl [CicAst.Symbol ("neq", 0); t1; t2])
- ]
- ];
-END
-
let _ =
let const s = Cic.Const (s, []) in
let mutind s = Cic.MutInd (s, 0, []) in
(fun _ num _ ->
let num = int_of_string num in
if num = 0 then
- raise DisambiguateChoices.Invalid_choice
+ raise DisambiguateTypes.Invalid_choice
else
HelmLibraryObjects.build_bin_pos num));
DisambiguateChoices.add_num_choice
HelmLibraryObjects.BinInt.zpos;
HelmLibraryObjects.build_bin_pos num ]
else
- assert false));
-
- DisambiguateChoices.add_binary_op "plus" "natural plus"
- HelmLibraryObjects.Peano.plus;
- DisambiguateChoices.add_binary_op "plus" "real plus"
- HelmLibraryObjects.Reals.rplus;
- DisambiguateChoices.add_binary_op "plus" "binary integer plus"
- HelmLibraryObjects.BinInt.zplus;
- DisambiguateChoices.add_binary_op "plus" "binary positive plus"
- HelmLibraryObjects.BinPos.pplus;
- DisambiguateChoices.add_binary_op "minus" "natural minus"
- (const HelmLibraryObjects.Peano.minus_URI);
- DisambiguateChoices.add_binary_op "minus" "real minus"
- (const HelmLibraryObjects.Reals.rminus_URI);
- DisambiguateChoices.add_binary_op "minus" "binary integer minus"
- HelmLibraryObjects.BinInt.zminus;
- DisambiguateChoices.add_binary_op "minus" "binary positive minus"
- HelmLibraryObjects.BinPos.pminus;
- DisambiguateChoices.add_binary_op "times" "natural times"
- (const HelmLibraryObjects.Peano.mult_URI);
- DisambiguateChoices.add_binary_op "times" "real times"
- (const HelmLibraryObjects.Reals.rmult_URI);
- DisambiguateChoices.add_binary_op "times" "binary positive times"
- HelmLibraryObjects.BinPos.pmult;
- DisambiguateChoices.add_binary_op "times" "binary integer times"
- HelmLibraryObjects.BinInt.zmult;
- DisambiguateChoices.add_binary_op "power" "real power"
- (const HelmLibraryObjects.Reals.pow_URI);
- DisambiguateChoices.add_binary_op "power" "integer power"
- (const HelmLibraryObjects.BinInt.zpower_URI);
- DisambiguateChoices.add_binary_op "divide" "real divide"
- (const HelmLibraryObjects.Reals.rdiv_URI);
- DisambiguateChoices.add_unary_op "uminus" "real unary minus"
- (const HelmLibraryObjects.Reals.ropp_URI);
- DisambiguateChoices.add_unary_op "uminus" "binary integer negative sign"
- (HelmLibraryObjects.BinInt.zneg);
- DisambiguateChoices.add_unary_op "uminus" "binary integer unary minus"
- (HelmLibraryObjects.BinInt.zopp);
-
- DisambiguateChoices.add_binary_op "leq" "natural 'less or equal to'"
- (mutind HelmLibraryObjects.Peano.le_URI);
- DisambiguateChoices.add_binary_op "leq" "real 'less or equal to'"
- (const HelmLibraryObjects.Reals.rle_URI);
- DisambiguateChoices.add_binary_op "geq" "natural 'greater or equal to'"
- (const HelmLibraryObjects.Peano.ge_URI);
- DisambiguateChoices.add_binary_op "geq" "real 'greater or equal to'"
- (const HelmLibraryObjects.Reals.rge_URI);
- DisambiguateChoices.add_binary_op "lt" "natural 'less than'"
- (const HelmLibraryObjects.Peano.lt_URI);
- DisambiguateChoices.add_binary_op "lt" "real 'less than'"
- (const HelmLibraryObjects.Reals.rlt_URI);
- DisambiguateChoices.add_binary_op "gt" "natural 'greater than'"
- (const HelmLibraryObjects.Peano.gt_URI);
- DisambiguateChoices.add_binary_op "gt" "real 'greater than'"
- (const HelmLibraryObjects.Reals.rgt_URI);
- DisambiguateChoices.add_symbol_choice "neq"
- ("not equal to (leibnitz)",
- (fun env _ args ->
- let t1, t2 =
- match args with
- | [t1; t2] -> t1, t2
- | _ -> raise DisambiguateChoices.Invalid_choice
- in
- Cic.Appl [ const HelmLibraryObjects.Logic.not_URI;
- Cic.Appl [
- Cic.MutInd (HelmLibraryObjects.Logic.eq_URI, 0, []);
- Cic.Implicit (Some `Type); t1; t2 ] ]));
+ assert false))
-(* vim:set encoding=utf8: *)
let choices_avg = ref 0.
*)
+let floc_of_loc (loc_begin, loc_end) =
+ let floc_begin =
+ { Lexing.pos_fname = ""; Lexing.pos_lnum = -1; Lexing.pos_bol = -1;
+ Lexing.pos_cnum = loc_begin }
+ in
+ let floc_end = { floc_begin with Lexing.pos_cnum = loc_end } in
+ (floc_begin, floc_end)
+
+let dummy_floc = floc_of_loc (-1, -1)
+
let descr_of_domain_item = function
| Id s -> s
| Symbol (s, _) -> s
(DisambiguateTypes.string_of_domain_item item))
(* TODO move it to Cic *)
-let find_in_environment name context =
+let find_in_environment name (context: Cic.name list) =
let rec aux acc = function
| [] -> raise Not_found
| Cic.Name hd :: tl when hd = name -> acc
in
aux 1 context
-let interpretate_term ~context ~env ~uri ~is_path ast =
+let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast =
assert (uri = None);
- let rec aux loc context = function
- | CicAst.AttributedTerm (`Loc loc, term) ->
+ let rec aux loc (context: Cic.name list) = function
+ | CicNotationPt.AttributedTerm (`Loc loc, term) ->
aux loc context term
- | CicAst.AttributedTerm (_, term) -> aux loc context term
- | CicAst.Appl (CicAst.Symbol (symb, i) :: args) ->
+ | CicNotationPt.AttributedTerm (_, term) -> aux loc context term
+ | CicNotationPt.Appl (CicNotationPt.Symbol (symb, i) :: args) ->
let cic_args = List.map (aux loc context) args in
resolve env (Symbol (symb, i)) ~args:cic_args ()
- | CicAst.Appl terms -> Cic.Appl (List.map (aux loc context) terms)
- | CicAst.Binder (binder_kind, (var, typ), body) ->
+ | CicNotationPt.Appl terms -> Cic.Appl (List.map (aux loc context) terms)
+ | CicNotationPt.Binder (binder_kind, (var, typ), body) ->
let cic_type = aux_option loc context (Some `Type) typ in
- let cic_body = aux loc (var :: context) body in
+ let cic_name = CicNotationUtil.cic_name_of_name var in
+ let cic_body = aux loc (cic_name :: context) body in
(match binder_kind with
- | `Lambda -> Cic.Lambda (var, cic_type, cic_body)
- | `Pi | `Forall -> Cic.Prod (var, cic_type, cic_body)
+ | `Lambda -> Cic.Lambda (cic_name, cic_type, cic_body)
+ | `Pi
+ | `Forall -> Cic.Prod (cic_name, cic_type, cic_body)
| `Exists ->
resolve env (Symbol ("exists", 0))
- ~args:[ cic_type; Cic.Lambda (var, cic_type, cic_body) ] ())
- | CicAst.Case (term, indty_ident, outtype, branches) ->
+ ~args:[ cic_type; Cic.Lambda (cic_name, cic_type, cic_body) ] ())
+ | CicNotationPt.Case (term, indty_ident, outtype, branches) ->
let cic_term = aux loc context term in
let cic_outtype = aux_option loc context None outtype in
let do_branch ((head, args), term) =
let rec do_branch' context = function
| [] -> aux loc context term
| (name, typ) :: tl ->
- let cic_body = do_branch' (name :: context) tl in
+ let cic_name = CicNotationUtil.cic_name_of_name name in
+ let cic_body = do_branch' (cic_name :: context) tl in
let typ =
match typ with
| None -> Cic.Implicit (Some `Type)
| Some typ -> aux loc context typ
in
- Cic.Lambda (name, typ, cic_body)
+ Cic.Lambda (cic_name, typ, cic_body)
in
do_branch' context args
in
(match resolve env (Id indty_ident) () with
| Cic.MutInd (uri, tyno, _) -> (uri, tyno)
| Cic.Implicit _ -> raise Try_again
- | _ -> raise DisambiguateChoices.Invalid_choice)
+ | _ -> raise Invalid_choice)
| None ->
let fst_constructor =
match branches with
| ((head, _), _) :: _ -> head
- | [] -> raise DisambiguateChoices.Invalid_choice
+ | [] -> raise Invalid_choice
in
(match resolve env (Id fst_constructor) () with
| Cic.MutConstruct (indtype_uri, indtype_no, _, _) ->
(indtype_uri, indtype_no)
| Cic.Implicit _ -> raise Try_again
- | _ -> raise DisambiguateChoices.Invalid_choice)
+ | _ -> raise Invalid_choice)
in
Cic.MutCase (indtype_uri, indtype_no, cic_outtype, cic_term,
(List.map do_branch branches))
- | CicAst.LetIn ((name, typ), def, body) ->
+ | CicNotationPt.Cast (t1, t2) ->
+ let cic_t1 = aux loc context t1 in
+ let cic_t2 = aux loc context t2 in
+ Cic.Cast (cic_t1, cic_t2)
+ | CicNotationPt.LetIn ((name, typ), def, body) ->
let cic_def = aux loc context def in
+ let cic_name = CicNotationUtil.cic_name_of_name name in
let cic_def =
match typ with
| None -> cic_def
| Some t -> Cic.Cast (cic_def, aux loc context t)
in
- let cic_body = aux loc (name :: context) body in
- Cic.LetIn (name, cic_def, cic_body)
- | CicAst.LetRec (kind, defs, body) ->
+ let cic_body = aux loc (cic_name :: context) body in
+ Cic.LetIn (cic_name, cic_def, cic_body)
+ | CicNotationPt.LetRec (kind, defs, body) ->
let context' =
- List.fold_left (fun acc ((name, _), _, _) -> name :: acc)
+ List.fold_left
+ (fun acc ((name, _), _, _) ->
+ CicNotationUtil.cic_name_of_name name :: acc)
context defs
in
let cic_body = aux loc context' body in
let cic_body = aux loc context' body in
let cic_type = aux_option loc context (Some `Type) typ in
let name =
- match name with
+ match CicNotationUtil.cic_name_of_name name with
| Cic.Anonymous ->
- CicTextualParser2.fail loc
+ CicNotationPt.fail loc
"Recursive functions cannot be anonymous"
| Cic.Name name -> name
in
Cic.LetIn (Cic.Name var, Cic.CoFix (!counter, funs), cic))
in
List.fold_right (build_term inductiveFuns) inductiveFuns cic_body
- | CicAst.Ident _
- | CicAst.Uri _ when is_path -> raise PathNotWellFormed
- | CicAst.Ident (name, subst)
- | CicAst.Uri (name, subst) as ast ->
- let is_uri = function CicAst.Uri _ -> true | _ -> false in
+ | CicNotationPt.Ident _
+ | CicNotationPt.Uri _ when is_path -> raise PathNotWellFormed
+ | CicNotationPt.Ident (name, subst)
+ | CicNotationPt.Uri (name, subst) as ast ->
+ let is_uri = function CicNotationPt.Uri _ -> true | _ -> false in
(try
if is_uri ast then raise Not_found;(* don't search the env for URIs *)
let index = find_in_environment name context in
if subst <> None then
- CicTextualParser2.fail loc
- "Explicit substitutions not allowed here";
+ CicNotationPt.fail loc "Explicit substitutions not allowed here";
Cic.Rel index
with Not_found ->
let cic =
try
CicUtil.term_of_uri (UriManager.uri_of_string name)
with UriManager.IllFormedUri _ ->
- CicTextualParser2.fail loc "Ill formed URI"
+ CicNotationPt.fail loc "Ill formed URI"
else
resolve env (Id name) ()
in
(try
List.assoc s ids_to_uris, aux loc context term
with Not_found ->
- raise DisambiguateChoices.Invalid_choice))
+ raise Invalid_choice))
subst
| None -> List.map (fun uri -> uri, Cic.Implicit None) uris)
in
(CicPp.ppterm t)
(String.concat "; "
(List.map
- (fun (s, term) -> s ^ " := " ^ CicAstPp.pp_term term)
+ (fun (s, term) -> s ^ " := " ^ CicNotationPtPp.pp_term term)
subst)));
*)
t
| _ ->
- raise DisambiguateChoices.Invalid_choice
+ raise Invalid_choice
with
CicEnvironment.CircularDependency _ ->
- raise DisambiguateChoices.Invalid_choice))
- | CicAst.Implicit -> Cic.Implicit None
- | CicAst.UserInput -> Cic.Implicit (Some `Hole)
- | CicAst.Num (num, i) -> resolve env (Num i) ~num ()
- | CicAst.Meta (index, subst) ->
+ raise Invalid_choice))
+ | CicNotationPt.Implicit -> Cic.Implicit None
+ | CicNotationPt.UserInput -> Cic.Implicit (Some `Hole)
+ | CicNotationPt.Num (num, i) -> resolve env (Num i) ~num ()
+ | CicNotationPt.Meta (index, subst) ->
let cic_subst =
List.map
(function None -> None | Some term -> Some (aux loc context term))
subst
in
Cic.Meta (index, cic_subst)
- | CicAst.Sort `Prop -> Cic.Sort Cic.Prop
- | CicAst.Sort `Set -> Cic.Sort Cic.Set
- | CicAst.Sort `Type -> Cic.Sort (Cic.Type (CicUniv.fresh())) (* TASSI *)
- | CicAst.Sort `CProp -> Cic.Sort Cic.CProp
- | CicAst.Symbol (symbol, instance) ->
+ | CicNotationPt.Sort `Prop -> Cic.Sort Cic.Prop
+ | CicNotationPt.Sort `Set -> Cic.Sort Cic.Set
+ | CicNotationPt.Sort `Type -> Cic.Sort (Cic.Type (CicUniv.fresh())) (* TASSI *)
+ | CicNotationPt.Sort `CProp -> Cic.Sort Cic.CProp
+ | CicNotationPt.Symbol (symbol, instance) ->
resolve env (Symbol (symbol, instance)) ()
- and aux_option loc context annotation = function
+ | _ -> assert false (* god bless Bologna *)
+ and aux_option loc (context: Cic.name list) annotation = function
| None -> Cic.Implicit annotation
| Some term -> aux loc context term
in
match ast with
- | CicAst.AttributedTerm (`Loc loc, term) -> aux loc context term
- | term -> aux CicAst.dummy_floc context term
+ | CicNotationPt.AttributedTerm (`Loc loc, term) -> aux loc context term
+ | term -> aux dummy_floc context term
let interpretate_path ~context ~env path =
interpretate_term ~context ~env ~uri:None ~is_path:true path
assert (context = []);
assert (is_path = false);
match obj with
- | TacticAst.Inductive (params,tyl) ->
+ | GrafiteAst.Inductive (params,tyl) ->
let uri = match uri with Some uri -> uri | None -> assert false in
let context,params =
let context,res =
List.fold_left
(fun (context,res) (name,t) ->
- (Cic.Name name)::context,
+ Cic.Name name :: context,
(name, interpretate_term context env None false t)::res
) ([],[]) params
in
) tyl
in
Cic.InductiveDefinition (tyl,[],List.length params,[])
- | TacticAst.Record (params,name,ty,fields) ->
+ | GrafiteAst.Record (params,name,ty,fields) ->
let uri = match uri with Some uri -> uri | None -> assert false in
let context,params =
let context,res =
List.fold_left
(fun (context,res) (name,t) ->
- (Cic.Name name)::context,
+ (Cic.Name name :: context),
(name, interpretate_term context env None false t)::res
) ([],[]) params
in
snd (
List.fold_left
(fun (context,res) (name,ty) ->
- let context' = (Cic.Name name)::context in
+ let context' = Cic.Name name :: context in
context',(name,interpretate_term context env None false ty)::res
) (context,[]) fields) in
let concl =
let field_names = List.map fst fields in
Cic.InductiveDefinition
(tyl,[],List.length params,[`Class (`Record field_names)])
- | TacticAst.Theorem (flavour, name, ty, bo) ->
+ | GrafiteAst.Theorem (flavour, name, ty, bo) ->
let attrs = [`Flavour flavour] in
let ty' = interpretate_term [] env None false ty in
(match bo with
(* "aux" keeps domain in reverse order and doesn't care about duplicates.
* Domain item more in deep in the list will be processed first.
*)
-let rec domain_rev_of_term ?(loc = CicAst.dummy_floc) context = function
- | CicAst.AttributedTerm (`Loc loc, term) ->
+let rec domain_rev_of_term ?(loc = dummy_floc) context = function
+ | CicNotationPt.AttributedTerm (`Loc loc, term) ->
domain_rev_of_term ~loc context term
- | CicAst.AttributedTerm (_, term) -> domain_rev_of_term ~loc context term
- | CicAst.Appl terms ->
+ | CicNotationPt.AttributedTerm (_, term) ->
+ domain_rev_of_term ~loc context term
+ | CicNotationPt.Appl terms ->
List.fold_left
(fun dom term -> domain_rev_of_term ~loc context term @ dom) [] terms
- | CicAst.Binder (kind, (var, typ), body) ->
+ | CicNotationPt.Binder (kind, (var, typ), body) ->
let kind_dom =
match kind with
| `Exists -> [ Symbol ("exists", 0) ]
| _ -> []
in
let type_dom = domain_rev_of_term_option loc context typ in
- let body_dom = domain_rev_of_term ~loc (var :: context) body in
+ let body_dom =
+ domain_rev_of_term ~loc
+ (CicNotationUtil.cic_name_of_name var :: context) body
+ in
body_dom @ type_dom @ kind_dom
- | CicAst.Case (term, indty_ident, outtype, branches) ->
+ | CicNotationPt.Case (term, indty_ident, outtype, branches) ->
let term_dom = domain_rev_of_term ~loc context term in
let outtype_dom = domain_rev_of_term_option loc context outtype in
let get_first_constructor = function
let (term_context, args_domain) =
List.fold_left
(fun (cont, dom) (name, typ) ->
- (name :: cont,
+ (CicNotationUtil.cic_name_of_name name :: cont,
(match typ with
| None -> dom
| Some typ -> domain_rev_of_term ~loc cont typ @ dom)))
(match indty_ident with
| None -> get_first_constructor branches
| Some ident -> [ Id ident ])
- | CicAst.LetIn ((var, typ), body, where) ->
+ | CicNotationPt.Cast (term, ty) ->
+ let term_dom = domain_rev_of_term ~loc context term in
+ let ty_dom = domain_rev_of_term ~loc context ty in
+ ty_dom @ term_dom
+ | CicNotationPt.LetIn ((var, typ), body, where) ->
let body_dom = domain_rev_of_term ~loc context body in
let type_dom = domain_rev_of_term_option loc context typ in
- let where_dom = domain_rev_of_term ~loc (var :: context) where in
+ let where_dom =
+ domain_rev_of_term ~loc
+ (CicNotationUtil.cic_name_of_name var :: context) where
+ in
where_dom @ type_dom @ body_dom
- | CicAst.LetRec (kind, defs, where) ->
+ | CicNotationPt.LetRec (kind, defs, where) ->
let context' =
- List.fold_left (fun acc ((var, typ), _, _) -> var :: acc)
+ List.fold_left
+ (fun acc ((var, typ), _, _) ->
+ CicNotationUtil.cic_name_of_name var :: acc)
context defs
in
let where_dom = domain_rev_of_term ~loc context' where in
[] defs
in
where_dom @ defs_dom
- | CicAst.Ident (name, subst) ->
+ | CicNotationPt.Ident (name, subst) ->
(try
let index = find_in_environment name context in
if subst <> None then
- CicTextualParser2.fail loc
- "Explicit substitutions not allowed here"
+ CicNotationPt.fail loc "Explicit substitutions not allowed here"
else
[]
with Not_found ->
let dom' = domain_rev_of_term ~loc context term in
dom' @ dom)
[Id name] subst))
- | CicAst.Uri _ -> []
- | CicAst.Implicit -> []
- | CicAst.Num (num, i) -> [ Num i ]
- | CicAst.Meta (index, local_context) ->
+ | CicNotationPt.Uri _ -> []
+ | CicNotationPt.Implicit -> []
+ | CicNotationPt.Num (num, i) -> [ Num i ]
+ | CicNotationPt.Meta (index, local_context) ->
List.fold_left
(fun dom term -> domain_rev_of_term_option loc context term @ dom) []
local_context
- | CicAst.Sort _ -> []
- | CicAst.Symbol (symbol, instance) -> [ Symbol (symbol, instance) ]
- | CicAst.UserInput -> assert false
+ | CicNotationPt.Sort _ -> []
+ | CicNotationPt.Symbol (symbol, instance) -> [ Symbol (symbol, instance) ]
+ | CicNotationPt.UserInput
+ | CicNotationPt.Literal _
+ | CicNotationPt.Layout _
+ | CicNotationPt.Magic _
+ | CicNotationPt.Variable _ -> assert false
and domain_rev_of_term_option loc context = function
| None -> []
assert (context = []);
let domain_rev =
match ast with
- | TacticAst.Theorem (_,_,ty,bo) ->
+ | GrafiteAst.Theorem (_,_,ty,bo) ->
(match bo with
None -> []
| Some bo -> domain_rev_of_term [] bo) @
domain_of_term [] ty
- | TacticAst.Inductive (params,tyl) ->
+ | GrafiteAst.Inductive (params,tyl) ->
let dom =
List.flatten (
List.rev_map
not ( List.exists (fun (name',_) -> name = Id name') params
|| List.exists (fun (name',_,_,_) -> name = Id name') tyl)
) dom
- | TacticAst.Record (params,_,ty,fields) ->
+ | GrafiteAst.Record (params,_,ty,fields) ->
let dom =
List.flatten
(List.rev_map (fun (_,ty) -> domain_rev_of_term [] ty) fields) in
metasenv:Cic.metasenv ->
?initial_ugraph:CicUniv.universe_graph ->
aliases:environment -> (* previous interpretation status *)
- CicAst.term ->
+ CicNotationPt.term ->
(environment * (* new interpretation status *)
Cic.metasenv * (* new metasenv *)
Cic.term*
dbd:Mysql.dbd ->
aliases:environment -> (* previous interpretation status *)
uri:UriManager.uri option -> (* required only for inductive types *)
- TacticAst.obj ->
+ GrafiteAst.obj ->
(environment * (* new interpretation status *)
Cic.metasenv * (* new metasenv *)
Cic.obj *
let choices = choices_of_id dbd id in
Hashtbl.add id_choices id choices;
choices)
- | Symbol (symb, _) -> DisambiguateChoices.lookup_symbol_choices symb
+ | Symbol (symb, _) ->
+ List.map DisambiguateChoices.mk_choice
+ (CicNotationRew.lookup_interpretations symb)
+(* DisambiguateChoices.lookup_symbol_choices symb *)
| Num instance -> DisambiguateChoices.lookup_num_choices ()
in
if choices = [] then raise (No_choices item);
let k,ugraph1 = refine_thing metasenv context uri cic_thing ugraph in
(k , ugraph1 )
with
- | Try_again -> Uncertain,ugraph
- | DisambiguateChoices.Invalid_choice -> Ko,ugraph
+ | Try_again -> Uncertain, ugraph
+ | Invalid_choice -> Ko, ugraph
in
(* (4) build all possible interpretations *)
let rec aux current_env todo_dom base_univ =
?(initial_ugraph = CicUniv.empty_ugraph) ~aliases term
=
disambiguate_thing ~dbd ~context ~metasenv ~initial_ugraph ~aliases
- ~uri:None ~pp_thing:CicAstPp.pp_term ~domain_of_thing:domain_of_term
+ ~uri:None ~pp_thing:CicNotationPp.pp_term ~domain_of_thing:domain_of_term
~interpretate_thing:interpretate_term ~refine_thing:refine_term term
let disambiguate_obj ~dbd ~aliases ~uri obj =
disambiguate_thing ~dbd ~context:[] ~metasenv:[] ~aliases ~uri
- ~pp_thing:TacticAstPp.pp_obj ~domain_of_thing:domain_of_obj
+ ~pp_thing:GrafiteAstPp.pp_obj ~domain_of_thing:domain_of_obj
~interpretate_thing:interpretate_obj ~refine_thing:refine_obj
obj
end
let input_or_locate_uri ~(title:string) ?id = raise Exit
end
module Disambiguator = Make (Callbacks)
- let disambiguate_string ~dbd ?(context=[]) ?(metasenv=[]) ?initial_ugraph
- ?(aliases=DisambiguateTypes.Environment.empty) term =
- let ast = CicTextualParser2.parse_term (Stream.of_string term) in
+ let disambiguate_string ~dbd ?(context = []) ?(metasenv = []) ?initial_ugraph
+ ?(aliases = DisambiguateTypes.Environment.empty) term
+ =
+ let ast = CicNotationParser.parse_level2_ast (Stream.of_string term) in
try
Disambiguator.disambiguate_term ~dbd ~context ~metasenv ast
?initial_ugraph ~aliases
exception PathNotWellFormed
val interpretate_path :
- context:Cic.name list -> env:DisambiguateTypes.environment -> CicAst.term ->
- Cic.term
-
+ context:Cic.name list -> env:DisambiguateTypes.environment ->
+ DisambiguateTypes.term ->
+ Cic.term
module type Disambiguator =
sig
metasenv:Cic.metasenv ->
?initial_ugraph:CicUniv.universe_graph ->
aliases:DisambiguateTypes.environment ->(* previous interpretation status *)
- CicAst.term ->
+ DisambiguateTypes.term ->
(DisambiguateTypes.environment * (* new interpretation status *)
Cic.metasenv * (* new metasenv *)
Cic.term *
dbd:Mysql.dbd ->
aliases:DisambiguateTypes.environment ->(* previous interpretation status *)
uri:UriManager.uri option -> (* required only for inductive types *)
- TacticAst.obj ->
+ GrafiteAst.obj ->
(DisambiguateTypes.environment * (* new interpretation status *)
Cic.metasenv * (* new metasenv *)
Cic.obj *
Cic.term *
CicUniv.universe_graph) list (* disambiguated term *)
end
+
+val dummy_floc: Lexing.position * Lexing.position
+
exception Invalid_choice
exception Choice_not_found of string
-let symbol_choices = Hashtbl.create 1023
let num_choices = ref []
-let add_symbol_choice symbol codomain_item =
- let current_choices =
- try
- Hashtbl.find symbol_choices symbol
- with Not_found -> []
- in
- Hashtbl.replace symbol_choices symbol (codomain_item :: current_choices)
-
-let add_binary_op symbol dsc appl_head =
- add_symbol_choice symbol
- (dsc,
- (fun env _ args ->
- let t1, t2 =
- match args with
- | [t1; t2] -> t1, t2
- | _ -> raise Invalid_choice
- in
- Cic.Appl [ appl_head; t1; t2 ]))
-
-let add_unary_op symbol dsc appl_head =
- add_symbol_choice symbol
- (dsc,
- (fun env _ args ->
- let t = match args with [t] -> t | _ -> raise Invalid_choice in
- Cic.Appl [ appl_head; t ]))
-
let add_num_choice choice = num_choices := choice :: !num_choices
-let lookup_symbol_choices symbol =
- try
- Hashtbl.find symbol_choices symbol
- with Not_found -> []
-
-let lookup_num_choices () = !num_choices
-
let has_description dsc = (fun x -> fst x = dsc)
-let lookup_symbol_by_dsc symb dsc =
- try
- List.find (has_description dsc) (Hashtbl.find symbol_choices symb)
- with Not_found ->
- raise (Choice_not_found (sprintf "Symbol %s, dsc %s" symb dsc))
+let lookup_num_choices () = !num_choices
let lookup_num_by_dsc dsc =
try
List.find (has_description dsc) !num_choices
with Not_found -> raise (Choice_not_found ("Num with dsc " ^ dsc))
- (** initial table contents *)
-
-let _ =
- add_binary_op "exists" "exists"
- (Cic.MutInd (HelmLibraryObjects.Logic.ex_URI, 0, []));
- add_symbol_choice "cast"
- ("type cast",
- (fun env _ args ->
- let t1, t2 =
- match args with
- | [t1; t2] -> t1, t2
- | _ -> raise Invalid_choice
- in
- Cic.Cast (t1, t2)));
+let mk_choice (dsc, args, appl_pattern) =
+ dsc,
+ (fun env _ cic_args ->
+ let env' =
+ let names =
+ List.map (function CicNotationPt.IdentArg (_, name) -> name) args
+ in
+ try
+ List.combine names cic_args
+ with Invalid_argument _ -> raise Invalid_choice
+ in
+ CicNotationFwd.instantiate_appl_pattern env' appl_pattern)
+
+let lookup_symbol_by_dsc symbol dsc =
+ try
+ mk_choice
+ (List.find
+ (fun (dsc', _, _) -> dsc = dsc')
+ (CicNotationRew.lookup_interpretations symbol))
+ with CicNotationRew.Interpretation_not_found | Not_found ->
+ raise (Choice_not_found (sprintf "Symbol %s, dsc %s" symbol dsc))
(** {2 Choice registration low-level interface} *)
- (** to be raised when a choice is invalid due to some given parameter (e.g.
- * wrong number of Cic.term arguments received) *)
-exception Invalid_choice
-
(** raised by lookup_XXXX below *)
exception Choice_not_found of string
- (** register a new symbol choice *)
-val add_symbol_choice: string -> codomain_item -> unit
-
(** register a new number choice *)
val add_num_choice: codomain_item -> unit
-(** {2 Choice registration high-level interface} *)
-
- (** @param symbol
- * @param description
- * @param term cic application head *)
-val add_binary_op: string -> string -> Cic.term -> unit
-
- (** @param symbol
- * @param description
- * @param term cic application head *)
-val add_unary_op: string -> string -> Cic.term -> unit
-
(** {2 Choices lookup}
* for user defined aliases *)
- (** @param symbol symbol as per AST *)
-val lookup_symbol_choices: string -> codomain_item list
-
val lookup_num_choices: unit -> codomain_item list
+ (** @param dsc description (1st component of codomain_item) *)
+val lookup_num_by_dsc: string -> codomain_item
+
(** @param symbol symbol as per AST
* @param dsc description (1st component of codomain_item)
*)
val lookup_symbol_by_dsc: string -> string -> codomain_item
- (** @param dsc description (1st component of codomain_item) *)
-val lookup_num_by_dsc: string -> codomain_item
+val mk_choice:
+ string * CicNotationPt.argument_pattern list *
+ CicNotationPt.cic_appl_pattern ->
+ codomain_item
--- /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/
+ *)
+
+open DisambiguateTypes
+
+let pp_environment env =
+ let aliases =
+ Environment.fold
+ (fun domain_item (dsc, _) acc ->
+ let s =
+ match domain_item with
+ | Id id ->
+ GrafiteAstPp.pp_alias (GrafiteAst.Ident_alias (id, dsc)) ^ "."
+ | Symbol (symb, i) ->
+ GrafiteAstPp.pp_alias (GrafiteAst.Symbol_alias (symb, i, dsc))
+ ^ "."
+ | Num i ->
+ GrafiteAstPp.pp_alias (GrafiteAst.Number_alias (i, dsc)) ^ "."
+ in
+ s :: acc)
+ env []
+ in
+ String.concat "\n" (List.sort compare aliases) ^
+ (if aliases = [] then "" else "\n")
+
--- /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/
+ *)
+
+val pp_environment: DisambiguateTypes.environment -> string
+
* http://helm.cs.unibo.it/
*)
-type term = CicAst.term
-type tactic = (term, string) TacticAst.tactic
-type tactical = (term, string) TacticAst.tactical
-type script_entry = Command of tactical | Comment of CicAst.location * string
-type script = CicAst.location * script_entry list
+type term = CicNotationPt.term
+type tactic = (term, string) GrafiteAst.tactic
+type tactical = (term, string) GrafiteAst.tactical
+type script_entry =
+ | Command of tactical
+ | Comment of CicNotationPt.location * string
+type script = CicNotationPt.location * script_entry list
type domain_item =
- | Id of string (* literal *)
- | Symbol of string * int (* literal, instance num *)
- | Num of int (* instance num *)
+ | Id of string (* literal *)
+ | Symbol of string * int (* literal, instance num *)
+ | Num of int (* instance num *)
+
+exception Invalid_choice
module OrderedDomain =
struct
(* module Domain: Set.S with type elt = domain_item *)
module Environment: Map.S with type key = domain_item
+ (** to be raised when a choice is invalid due to some given parameter (e.g.
+ * wrong number of Cic.term arguments received) *)
+exception Invalid_choice
+
type codomain_item =
string * (* description *)
(environment -> string -> Cic.term list -> Cic.term)
(** {3 type shortands} *)
-type term = CicAst.term
-type tactic = (term, string) TacticAst.tactic
-type tactical = (term, string) TacticAst.tactical
+type term = CicNotationPt.term
+type tactic = (term, string) GrafiteAst.tactic
+type tactical = (term, string) GrafiteAst.tactical
type script_entry =
| Command of tactical
- | Comment of CicAst.location * string
-type script = CicAst.location * script_entry list
+ | Comment of CicNotationPt.location * string
+type script = CicNotationPt.location * script_entry list
val empty_environment: environment
-cicNotationUtil.cmi: grafiteAst.cmo cicNotationPt.cmo
+cicNotationUtil.cmi: cicNotationPt.cmo
cicNotationTag.cmi: cicNotationPt.cmo
cicNotationEnv.cmi: cicNotationPt.cmo
cicNotationPp.cmi: cicNotationPt.cmo cicNotationEnv.cmi
-cicNotationMatcher.cmi: grafiteAst.cmo cicNotationPt.cmo cicNotationEnv.cmi
+grafiteAstPp.cmi: grafiteAst.cmo cicNotationPt.cmo
+cicNotationMatcher.cmi: cicNotationPt.cmo cicNotationEnv.cmi
cicNotationFwd.cmi: cicNotationPt.cmo cicNotationEnv.cmi
+cicNotationRew.cmi: cicNotationPt.cmo
cicNotationParser.cmi: cicNotationPt.cmo cicNotationEnv.cmi
grafiteParser.cmi: grafiteAst.cmo cicNotationPt.cmo
-cicNotationRew.cmi: grafiteAst.cmo cicNotationPt.cmo
cicNotationPres.cmi: cicNotationPt.cmo
+cicNotation.cmi: grafiteAst.cmo
grafiteAst.cmo: cicNotationPt.cmo
grafiteAst.cmx: cicNotationPt.cmx
-cicNotationUtil.cmo: grafiteAst.cmo cicNotationPt.cmo cicNotationUtil.cmi
-cicNotationUtil.cmx: grafiteAst.cmx cicNotationPt.cmx cicNotationUtil.cmi
+cicNotationUtil.cmo: cicNotationPt.cmo cicNotationUtil.cmi
+cicNotationUtil.cmx: cicNotationPt.cmx cicNotationUtil.cmi
cicNotationTag.cmo: cicNotationUtil.cmi cicNotationPt.cmo cicNotationTag.cmi
cicNotationTag.cmx: cicNotationUtil.cmx cicNotationPt.cmx cicNotationTag.cmi
cicNotationLexer.cmo: cicNotationLexer.cmi
cicNotationEnv.cmx: cicNotationUtil.cmx cicNotationPt.cmx cicNotationEnv.cmi
cicNotationPp.cmo: cicNotationPt.cmo cicNotationEnv.cmi cicNotationPp.cmi
cicNotationPp.cmx: cicNotationPt.cmx cicNotationEnv.cmx cicNotationPp.cmi
-cicNotationMatcher.cmo: grafiteAst.cmo cicNotationUtil.cmi cicNotationTag.cmi \
+grafiteAstPp.cmo: grafiteAst.cmo cicNotationPp.cmi grafiteAstPp.cmi
+grafiteAstPp.cmx: grafiteAst.cmx cicNotationPp.cmx grafiteAstPp.cmi
+cicNotationMatcher.cmo: cicNotationUtil.cmi cicNotationTag.cmi \
cicNotationPt.cmo cicNotationPp.cmi cicNotationEnv.cmi \
cicNotationMatcher.cmi
-cicNotationMatcher.cmx: grafiteAst.cmx cicNotationUtil.cmx cicNotationTag.cmx \
+cicNotationMatcher.cmx: cicNotationUtil.cmx cicNotationTag.cmx \
cicNotationPt.cmx cicNotationPp.cmx cicNotationEnv.cmx \
cicNotationMatcher.cmi
cicNotationFwd.cmo: cicNotationUtil.cmi cicNotationPt.cmo cicNotationEnv.cmi \
cicNotationFwd.cmi
cicNotationFwd.cmx: cicNotationUtil.cmx cicNotationPt.cmx cicNotationEnv.cmx \
cicNotationFwd.cmi
+cicNotationRew.cmo: cicNotationUtil.cmi cicNotationPt.cmo \
+ cicNotationMatcher.cmi cicNotationEnv.cmi cicNotationRew.cmi
+cicNotationRew.cmx: cicNotationUtil.cmx cicNotationPt.cmx \
+ cicNotationMatcher.cmx cicNotationEnv.cmx cicNotationRew.cmi
cicNotationParser.cmo: cicNotationUtil.cmi cicNotationPt.cmo \
cicNotationPp.cmi cicNotationLexer.cmi cicNotationEnv.cmi \
cicNotationParser.cmi
grafiteParser.cmi
grafiteParser.cmx: grafiteAst.cmx cicNotationPt.cmx cicNotationParser.cmx \
grafiteParser.cmi
-cicNotationRew.cmo: grafiteAst.cmo cicNotationUtil.cmi cicNotationPt.cmo \
- cicNotationParser.cmi cicNotationMatcher.cmi cicNotationEnv.cmi \
- cicNotationRew.cmi
-cicNotationRew.cmx: grafiteAst.cmx cicNotationUtil.cmx cicNotationPt.cmx \
- cicNotationParser.cmx cicNotationMatcher.cmx cicNotationEnv.cmx \
- cicNotationRew.cmi
cicNotationPres.cmo: cicNotationUtil.cmi cicNotationPt.cmo \
cicNotationPres.cmi cicNotationPp.cmi cicNotationPres.cmi
cicNotationPres.cmx: cicNotationUtil.cmx cicNotationPt.cmx \
cicNotationPres.cmx cicNotationPp.cmx cicNotationPres.cmi
+cicNotation.cmo: grafiteParser.cmi grafiteAst.cmo cicNotationRew.cmi \
+ cicNotationParser.cmi cicNotationFwd.cmi cicNotation.cmi
+cicNotation.cmx: grafiteParser.cmx grafiteAst.cmx cicNotationRew.cmx \
+ cicNotationParser.cmx cicNotationFwd.cmx cicNotation.cmi
cicNotationLexer.mli \
cicNotationEnv.mli \
cicNotationPp.mli \
+ grafiteAstPp.mli \
cicNotationMatcher.mli \
cicNotationFwd.mli \
+ cicNotationRew.mli \
cicNotationParser.mli \
grafiteParser.mli \
- cicNotationRew.mli \
cicNotationPres.mli \
+ cicNotation.mli \
$(NULL)
IMPLEMENTATION_FILES = \
cicNotationPt.ml \
TODO
-* implementare trasformazione 1 => 0
* gestione priorita'/associativita'
- triplicare livelli nella grammatica?
* implementare type-checker per le trasformazioni
* prestazioni trasformazioni 3 => 2 e 2 => 1
* magic per gestione degli array?
* gestione speciale dei numeri
-* sintassi concreta / prelexing
+* sintassi concreta
- studiare/implementare sintassi con ... per i magic fold
* integrazione
- - porting della disambiguazione al nuovo ast
- - apportare all'ast le modifiche di CicAst (case, cast non come annotazione,
- tipi opzionali nel let rec e nelle definizioni)
+ - portare le trasformazioni al nuovo ast
+ - salvare la notazione nei file .moo
+ - togliere file non piu' utilizzati (caterva di cvs remove)
DONE
+* implementare trasformazione 1 => 0
* implementare istanziazione dei magic a livello 1 (2 => 1)
* implementare compilazione dei default in 2 => 1
- -> Tue, 07 Jun 2005 17:17:36 +0200 zack
* annotazioni nel livello 1 generato
* problema con pattern overlapping per i magic al livello 2
* gestione greedyness dei magic in 2 => 1
* href multipli
+* integrazione
+ - apportare all'ast le modifiche di CicAst (case, cast non come annotazione,
+ tipi opzionali nel let rec e nelle definizioni)
+* integrazione
+ - porting della disambiguazione al nuovo ast
+ - refactoring: unico punto di accesso allo stato imperativo della notazione
+ - gestire cast
--- /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/
+ *)
+
+open GrafiteAst
+
+type notation_id =
+ | RuleId of CicNotationParser.rule_id
+ | InterpretationId of CicNotationRew.interpretation_id
+ | PrettyPrinterId of CicNotationRew.pretty_printer_id
+
+let process_notation st =
+ match st with
+ | Notation (loc, l1, associativity, precedence, l2) ->
+ let rule_id =
+ CicNotationParser.extend l1 ?precedence ?associativity
+ (fun env loc -> CicNotationFwd.instantiate_level2 env l2)
+ in
+ let pp_id =
+ CicNotationRew.add_pretty_printer ?precedence ?associativity l2 l1
+ in
+ st, [ RuleId rule_id; PrettyPrinterId pp_id ]
+ | Interpretation (loc, dsc, l2, l3) ->
+ let interp_id = CicNotationRew.add_interpretation dsc l2 l3 in
+ st, [ InterpretationId interp_id ]
+ | st -> st, []
+
+let remove_notation = function
+ | RuleId id -> CicNotationParser.delete id
+ | PrettyPrinterId id -> CicNotationRew.remove_pretty_printer id
+ | InterpretationId id -> CicNotationRew.remove_interpretation id
+
+let load_notation fname =
+ let ic = open_in fname in
+ let istream = Stream.of_channel ic in
+ try
+ while true do
+ match GrafiteParser.parse_statement istream with
+ | Executable (_, Command (_, cmd)) -> ignore (process_notation cmd)
+ | _ -> ()
+ done
+ with End_of_file -> close_in ic
+
--- /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/
+ *)
+
+type notation_id
+
+val process_notation:
+ ('a, 'b) GrafiteAst.command -> ('a, 'b) GrafiteAst.command * notation_id list
+
+val remove_notation: notation_id -> unit
+
+(** @param fname file from which load notation *)
+val load_notation: string -> unit
+
* http://helm.cs.unibo.it/
*)
+open Printf
+
open CicNotationEnv
open CicNotationPt
in
aux env term
+let instantiate_appl_pattern 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
+ | UriPattern uri -> CicUtil.term_of_uri uri
+ | ImplicitPattern -> Cic.Implicit None
+ | VarPattern name -> lookup name
+ | ApplPattern terms -> Cic.Appl (List.map aux terms)
+ in
+ aux appl_pattern
+
CicNotationEnv.t -> CicNotationPt.term ->
CicNotationPt.term
+ (** @param env environment from argument_pattern to cic terms
+ * @param pat cic_appl_pattern *)
+val instantiate_appl_pattern:
+ (string * Cic.term) list -> CicNotationPt.cic_appl_pattern ->
+ Cic.term
+
(* TODO ZACK: keyword list almost cut and paste from cicTextualLexer2.ml, to
* be reviewed *)
List.iter (fun k -> Hashtbl.add level2_ast_keywords k ())
- [ "Prop"; "Type"; "Set"; "let"; "rec"; "corec"; "match"; "with"; "in";
- "and"; "on" ]
+ [ "Prop"; "Type"; "Set"; "let"; "rec"; "corec"; "using"; "match"; "with";
+ "in"; "and"; "to"; "as"; "on"; "names" ]
let add_level2_ast_keyword k = Hashtbl.add level2_ast_keywords k ()
let remove_level2_ast_keyword k = Hashtbl.remove level2_ast_keywords k
| uri -> return lexbuf ("URI", Ulexing.utf8_lexeme lexbuf)
| qstring ->
return lexbuf ("QSTRING", remove_quotes (Ulexing.utf8_lexeme lexbuf))
- | csymbol -> return lexbuf ("CSYMBOL", Ulexing.utf8_lexeme lexbuf)
+ | csymbol ->
+ return lexbuf ("CSYMBOL", remove_left_quote (Ulexing.utf8_lexeme lexbuf))
| "${" -> read_unparsed_group "UNPARSED_META" lexbuf
| "@{" -> read_unparsed_group "UNPARSED_AST" lexbuf
| '(' -> return lexbuf ("LPAREN", "")
Hashtbl.hash mask, tl
let mask_of_appl_pattern = function
- | GrafiteAst.UriPattern uri -> Uri uri, []
- | GrafiteAst.VarPattern _ -> Blob, []
- | GrafiteAst.ApplPattern pl -> Appl (List.map (fun _ -> Blob) pl), pl
+ | Pt.UriPattern uri -> Uri uri, []
+ | Pt.ImplicitPattern
+ | Pt.VarPattern _ -> Blob, []
+ | Pt.ApplPattern pl -> Appl (List.map (fun _ -> Blob) pl), pl
let tag_of_pattern p =
let mask, pl = mask_of_appl_pattern p in
Hashtbl.hash mask, pl
- type pattern_t = GrafiteAst.cic_appl_pattern
+ type pattern_t = Pt.cic_appl_pattern
type term_t = Cic.annterm
let classify = function
- | GrafiteAst.VarPattern _ -> Variable
+ | Pt.VarPattern _ -> Variable
| _ -> Constructor
end
List.map2
(fun p t ->
match p with
- | GrafiteAst.VarPattern name -> name, t
+ | Pt.ImplicitPattern -> Util.fresh_name (), t
+ | Pt.VarPattern name -> name, t
| _ -> assert false)
pl matched_terms
in
module Matcher32:
sig
val compiler :
- (GrafiteAst.cic_appl_pattern * int) list ->
+ (CicNotationPt.cic_appl_pattern * int) list ->
(Cic.annterm -> ((string * Cic.annterm) list * int) option)
end
let max_precedence = 100
let default_precedence = 50
-let let_in_prec = 10
-let binder_prec = 20
-let apply_prec = 70
-let simple_prec = 90
-
-let let_in_assoc = Gramext.NonA
-let binder_assoc = Gramext.RightA
-let apply_assoc = Gramext.LeftA
-let simple_assoc = Gramext.NonA
-
let level1_pattern =
Grammar.Entry.create level1_pattern_grammar "level1_pattern"
let level2_ast = Grammar.Entry.create level2_ast_grammar "level2_ast"
let return_term loc term = ()
-let fail floc msg =
- let (x, y) = loc_of_floc floc in
- failwith (sprintf "Error at characters %d - %d: %s" x y msg)
-
let int_of_string s =
try
Pervasives.int_of_string s
SYMBOL "]" ->
return_term loc (Case (t, indty_ident, outtyp, patterns))
| LPAREN; p1 = term; SYMBOL ":"; p2 = term; RPAREN ->
- return_term loc (Appl [ Symbol ("cast", 0); p1; p2 ])
+ return_term loc (Cast (p1, p2))
| LPAREN; p = term; RPAREN -> p
| blob = UNPARSED_META -> !parse_level2_meta_ref (Stream.of_string blob)
]
val delete: rule_id -> unit
-(** {2 Standard precedences} *)
-
-val let_in_prec: int
-val binder_prec: int
-val apply_prec: int
-val simple_prec: int
-
-val let_in_assoc: Gramext.g_assoc
-val binder_assoc: Gramext.g_assoc
-val apply_assoc: Gramext.g_assoc
-val simple_assoc: Gramext.g_assoc
-
(** {2 Grammar entries}
* needed by grafite parser *)
sprintf "%smatch %s with %s"
(match typ with None -> "" | Some t -> sprintf "<%s>" (pp_term t))
(pp_term term) (pp_patterns patterns)
+ | Cast (t1, t2) -> sprintf "(%s: %s)" (pp_term t1) (pp_term t2)
| LetIn (var, t1, t2) ->
sprintf "let %s = %s in %s" (pp_capture_variable var) (pp_term t1)
(pp_term t2)
let loc_of_floc = function
| { Lexing.pos_cnum = loc_begin }, { Lexing.pos_cnum = loc_end } ->
(loc_begin, loc_end)
+let fail floc msg =
+ let (x, y) = loc_of_floc floc in
+ failwith (Printf.sprintf "Error at characters %d - %d: %s" x y msg)
type term_attribute =
[ `Loc of location (* source file location *)
| Binder of binder_kind * capture_variable * term (* kind, name, body *)
| Case of term * string option * term option * (case_pattern * term) list
(* what to match, inductive type, out type, <pattern,action> list *)
+ | Cast of term * term
| LetIn of capture_variable * term * term (* name, body, where *)
| LetRec of induction_kind * (capture_variable * term * int) list * term
(* (name, body, decreasing argument) list, where *)
(* level 2 variables *)
| FreshVar of string
+type argument_pattern =
+ | IdentArg of int * string (* eta-depth, name *)
+
+type cic_appl_pattern =
+ | UriPattern of UriManager.uri
+ | VarPattern of string
+ | ImplicitPattern
+ | ApplPattern of cic_appl_pattern list
+
+(** {2 Standard precedences} *)
+
+let let_in_prec = 10
+let binder_prec = 20
+let apply_prec = 70
+let simple_prec = 90
+
+let let_in_assoc = Gramext.NonA
+let binder_assoc = Gramext.RightA
+let apply_assoc = Gramext.LeftA
+let simple_assoc = Gramext.NonA
+
let default_prec = 50
let default_assoc = Gramext.NonA
+module Ast = CicNotationPt
+
type term_info =
- { sort: (Cic.id, CicNotationPt.sort_kind) Hashtbl.t;
+ { sort: (Cic.id, Ast.sort_kind) Hashtbl.t;
uri: (Cic.id, string) Hashtbl.t;
}
fst (List.nth (constructors_of_inductive_type uri i) (j-1))
with Not_found -> assert false)
-module Ast = CicNotationPt
-module Parser = CicNotationParser
-
-let string_of_name = function
- | Cic.Name s -> s
- | Cic.Anonymous -> "_"
-
-let ident_of_name n = Ast.Ident (string_of_name n, None)
-
let idref id t = Ast.AttributedTerm (`IdRef id, t)
let resolve_binder = function
in
let rec aux = function
| Ast.Appl ts ->
- Ast.AttributedTerm (`Level (Parser.apply_prec, Parser.apply_assoc),
+ Ast.AttributedTerm (`Level (Ast.apply_prec, Ast.apply_assoc),
Ast.Layout
(Ast.Box ((Ast.HOV, true, true),
(CicNotationUtil.dress
(List.map k ts)))))
| Ast.Binder (`Forall, (Ast.Ident ("_", _), ty), body)
| Ast.Binder (`Pi, (Ast.Ident ("_", _), ty), body) ->
- Ast.AttributedTerm (`Level (Parser.binder_prec, Parser.binder_assoc),
+ Ast.AttributedTerm (`Level (Ast.binder_prec, Ast.binder_assoc),
Ast.Layout (Ast.Box ((Ast.HV, false, true), [
aux_ty ty;
Ast.Layout Ast.Break;
binder_symbol "\\to";
k body])))
| Ast.Binder (binder_kind, (id, ty), body) ->
- Ast.AttributedTerm (`Level (Parser.binder_prec, Parser.binder_assoc),
+ Ast.AttributedTerm (`Level (Ast.binder_prec, Ast.binder_assoc),
Ast.Layout (Ast.Box ((Ast.HV, false, true), [
binder_symbol (resolve_binder binder_kind);
k id;
| `Set | `Type -> `Pi
| `Prop | `CProp -> `Forall
in
- idref id (Ast.Binder (binder_kind, (ident_of_name n, Some (k s)), k t))
- | Cic.ACast (id,v,t) ->
- idref id (Ast.Appl [idref id (Ast.Symbol ("cast", 0)); k v; k t])
+ idref id (Ast.Binder (binder_kind,
+ (CicNotationUtil.name_of_cic_name n, Some (k s)), k t))
+ | Cic.ACast (id,v,t) -> idref id (Ast.Cast (k v, k t))
| Cic.ALambda (id,n,s,t) ->
- idref id (Ast.Binder (`Lambda, (ident_of_name n, Some (k s)), k t))
+ idref id (Ast.Binder (`Lambda,
+ (CicNotationUtil.name_of_cic_name n, Some (k s)), k t))
| Cic.ALetIn (id,n,s,t) ->
- idref id (Ast.LetIn ((ident_of_name n, None), k s, k t))
+ idref id (Ast.LetIn ((CicNotationUtil.name_of_cic_name n, None),
+ k s, k t))
| Cic.AAppl (aid,args) -> idref aid (Ast.Appl (List.map k args))
| Cic.AConst (id,uri,substs) ->
register_uri id (UriManager.string_of_uri uri);
match (ty, pat) with
| Cic.Prod (_, _, t), Cic.ALambda (_, name, s, t') ->
let (cv, rhs) = eat_branch t t' in
- (ident_of_name name, Some (k s)) :: cv, rhs
+ (CicNotationUtil.name_of_cic_name name, Some (k s)) :: cv, rhs
| _, _ -> [], k pat
in
let patterns =
let level1_patterns21 = Hashtbl.create 211
let level2_patterns32 = Hashtbl.create 211
+let interpretations = Hashtbl.create 211 (* symb -> id list ref *)
let compiled21 = ref None
let compiled32 = ref None
let sep =
match sep_opt with
| None -> []
- | Some l -> [ CicNotationPt.Literal l ]
+ | Some l -> [ Ast.Literal l ]
in
let rec instantiate_list acc = function
| [] -> List.rev acc
let instantiate32 term_info env symbol args =
let rec instantiate_arg = function
- | GrafiteAst.IdentArg (n, name) ->
+ | Ast.IdentArg (n, name) ->
let t = (try List.assoc name env with Not_found -> assert false) in
let rec count_lambda = function
| Ast.Binder (`Lambda, _, body) -> 1 + count_lambda body
let env' =
List.map (fun (name, term) -> (name, ast_of_acic1 term_info term)) env
in
- let symbol, args, uris =
+ let _, symbol, args, _, uris =
try
Hashtbl.find level2_patterns32 pid
with Not_found -> assert false
incr counter;
!counter
-let add_interpretation (symbol, args) appl_pattern =
+let add_interpretation dsc (symbol, args) appl_pattern =
let id = fresh_id () in
let uris = CicNotationUtil.find_appl_pattern_uris appl_pattern in
- Hashtbl.add level2_patterns32 id (symbol, args, uris);
+ Hashtbl.add level2_patterns32 id (dsc, symbol, args, appl_pattern, uris);
pattern32_matrix := (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
+exception Interpretation_not_found
+exception Pretty_printer_not_found
+
+let lookup_interpretations symbol =
+ try
+ 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 add_pretty_printer
?(precedence = default_prec) ?(associativity = default_assoc) l2 l1
=
load_patterns21 !pattern21_matrix;
id
-exception Interpretation_not_found
-exception Pretty_printer_not_found
-
let remove_interpretation id =
(try
+ let _, 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;
type pretty_printer_id
val add_interpretation:
- string * GrafiteAst.argument_pattern list -> (* level 2 pattern *)
- GrafiteAst.cic_appl_pattern -> (* level 3 pattern *)
+ string -> (* id / description *)
+ string * CicNotationPt.argument_pattern list -> (* symbol, level 2 pattern *)
+ CicNotationPt.cic_appl_pattern -> (* level 3 pattern *)
interpretation_id
+ (** @raise Interpretation_not_found *)
+val lookup_interpretations:
+ string -> (* symbol *)
+ (string * CicNotationPt.argument_pattern list *
+ CicNotationPt.cic_appl_pattern) list
+
val add_pretty_printer:
?precedence:int ->
?associativity:Gramext.g_assoc ->
open CicNotationPt
- (* TODO ensure that names generated by fresh_var do not clash with user's *)
-let fresh_name =
- let index = ref ~-1 in
- fun () ->
- incr index;
- "fresh" ^ string_of_int !index
-
(* let meta_names_of term = *)
(* let rec names = ref [] in *)
(* let add_name n = *)
Binder (kind, aux_capture_variable var, k body)
| Case (term, indtype, typ, patterns) ->
Case (k term, indtype, aux_opt typ, aux_patterns patterns)
+ | Cast (t1, t2) -> Cast (k t1, k t2)
| LetIn (var, t1, t2) -> LetIn (aux_capture_variable var, k t1, k t2)
| LetRec (kind, definitions, term) ->
let definitions =
let find_appl_pattern_uris ap =
let rec aux acc =
function
- | GrafiteAst.UriPattern uri ->
+ | UriPattern uri ->
(try
ignore (List.find (fun uri' -> UriManager.eq uri uri') acc);
acc
with Not_found -> uri :: acc)
- | GrafiteAst.VarPattern _ -> acc
- | GrafiteAst.ApplPattern apl -> List.fold_left aux acc apl
+ | ImplicitPattern
+ | VarPattern _ -> acc
+ | ApplPattern apl -> List.fold_left aux acc apl
in
aux [] ap
Magic (If (_, Magic Fail, t)) -> find_branch t
| Magic (If (_, t, _)) -> find_branch t
| t -> t
+
+let cic_name_of_name = function
+ | CicNotationPt.Ident ("_", None) -> Cic.Anonymous
+ | CicNotationPt.Ident (name, None) -> Cic.Name name
+ | _ -> assert false
+
+let name_of_cic_name = function
+ | Cic.Name s -> CicNotationPt.Ident (s, None)
+ | Cic.Anonymous -> CicNotationPt.Ident ("_", None)
+
+let fresh_index = ref ~-1
+
+type notation_id = int
+
+let fresh_id () =
+ incr fresh_index;
+ !fresh_index
+
+ (* TODO ensure that names generated by fresh_var do not clash with user's *)
+let fresh_name () = "fresh" ^ string_of_int (fresh_id ())
+
val group: CicNotationPt.term list -> CicNotationPt.term
val ungroup: CicNotationPt.term list -> CicNotationPt.term list
-val find_appl_pattern_uris: GrafiteAst.cic_appl_pattern -> UriManager.uri list
+val find_appl_pattern_uris:
+ CicNotationPt.cic_appl_pattern -> UriManager.uri list
val find_branch:
CicNotationPt.term -> CicNotationPt.term
+
+val cic_name_of_name: CicNotationPt.term -> Cic.name
+val name_of_cic_name: Cic.name -> CicNotationPt.term
+
+ (** Notation id handling *)
+
+type notation_id
+
+val fresh_id: unit -> notation_id
+
+++ /dev/null
-notation "hvbox(a break \to b)"
- right associative with precedence 20
-for @{ \forall $_:$a.$b }.
-
-notation "hvbox(a break = b)"
- non associative with precedence 45
-for @{ 'eq $a $b }.
-
-notation "hvbox(a break \leq b)"
- non associative with precedence 45
-for @{ 'leq $a $b }.
-
-notation "hvbox(a break \geq b)"
- non associative with precedence 45
-for @{ 'geq $a $b }.
-
-notation "hvbox(a break \lt b)"
- non associative with precedence 45
-for @{ 'lt $a $b }.
-
-notation "hvbox(a break \gt b)"
- non associative with precedence 45
-for @{ 'gt $a $b }.
-
-notation "hvbox(a break \neq b)"
- non associative with precedence 45
-for @{ 'neq $a $b }.
-
-notation "hvbox(a break + b)"
- left associative with precedence 50
-for @{ 'plus $a $b }.
-
-notation "hvbox(a break - b)"
- left associative with precedence 50
-for @{ 'minus $a $b }.
-
-notation "hvbox(a break * b)"
- left associative with precedence 55
-for @{ 'times $a $b }.
-
-notation "hvbox(a break / b)"
- left associative with precedence 55
-for @{ 'divide $a $b }.
-
-notation "\frac a b"
- non associative with precedence 90
-for @{ 'divide $a $b }.
-
-notation "a \over b"
- non associative with precedence 55
-for @{ 'divide $a $b }.
-
-notation "- a"
- non associative with precedence 60
-for @{ 'uminus $a }.
-
-notation "\sqrt a"
- non associative with precedence 60
-for @{ 'sqrt $a }.
-
-notation "hvbox(a break \lor b)"
- left associative with precedence 30
-for @{ 'or $a $b }.
-
-notation "hvbox(a break \land b)"
- left associative with precedence 35
-for @{ 'or $a $b }.
-
-notation "hvbox(a break \lnot b)"
- left associative with precedence 40
-for @{ 'or $a $b }.
-
(string * CicNotationPt.term) list * string * CicNotationPt.term *
(string * CicNotationPt.term) list
-type argument_pattern =
- | IdentArg of int * string (* eta-depth, name *)
-
-type cic_appl_pattern =
- | UriPattern of UriManager.uri
- | VarPattern of string
- | ApplPattern of cic_appl_pattern list
-
type ('term,'obj) command =
| Default of loc * string * UriManager.uri list
| Include of loc * string
| Alias of loc * alias_spec
(** parameters, name, type, fields *)
| Obj of loc * 'obj
- | Notation of loc * 'term * Gramext.g_assoc option * int option * 'term
+ | Notation of loc * CicNotationPt.term * Gramext.g_assoc option * int option *
+ CicNotationPt.term
(* level 1 pattern, associativity, precedence, level 2 pattern *)
- | Interpretation of loc * (string * argument_pattern list) * cic_appl_pattern
+ | Interpretation of loc *
+ string * (string * CicNotationPt.argument_pattern list) *
+ CicNotationPt.cic_appl_pattern
+ (* description (i.e. id), symbol, arg pattern, appl pattern *)
(* DEBUGGING *)
| Dump of loc (* dump grammar on stdout *)
--- /dev/null
+(* Copyright (C) 2004, 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/
+ *)
+
+open Printf
+
+open GrafiteAst
+
+let tactical_terminator = "."
+let tactic_terminator = tactical_terminator
+let command_terminator = tactical_terminator
+
+let pp_term_ast term = CicNotationPp.pp_term term
+let pp_term_cic term = CicPp.ppterm term
+
+let pp_idents idents = "[" ^ String.concat "; " idents ^ "]"
+
+let pp_terms_ast terms = String.concat ", " (List.map pp_term_ast terms)
+
+let pp_reduction_kind = function
+ | `Reduce -> "reduce"
+ | `Simpl -> "simplify"
+ | `Whd -> "whd"
+ | `Normalize -> "normalize"
+
+
+let pp_pattern (t, hyp, goal) =
+ let pp_hyp_pattern l =
+ String.concat "; "
+ (List.map (fun (name, p) -> sprintf "%s : %s" name (pp_term_ast p)) l) in
+ let pp_t t =
+ match t with
+ None -> ""
+ | Some t -> pp_term_ast t
+ in
+ pp_t t ^ " in " ^ pp_hyp_pattern hyp ^ " \\vdash " ^ pp_term_ast goal
+
+let pp_intros_specs = function
+ | None, [] -> ""
+ | Some num, [] -> Printf.sprintf " names %i" num
+ | None, idents -> Printf.sprintf " names %s" (pp_idents idents)
+ | Some num, idents -> Printf.sprintf " names %i %s" num (pp_idents idents)
+
+let rec pp_tactic = function
+ | Absurd (_, term) -> "absurd" ^ pp_term_ast term
+ | Apply (_, term) -> "apply " ^ pp_term_ast term
+ | Auto _ -> "auto"
+ | Assumption _ -> "assumption"
+ | Change (_, where, with_what) ->
+ sprintf "change %s with %s" (pp_pattern where) (pp_term_ast with_what)
+ | Clear (_,id) -> sprintf "clear %s" id
+ | ClearBody (_,id) -> sprintf "clearbody %s" id
+ | Compare (_,term) -> "compare " ^ pp_term_ast term
+ | Constructor (_,n) -> "constructor " ^ string_of_int n
+ | Contradiction _ -> "contradiction"
+ | Cut (_, ident, term) ->
+ "cut " ^ pp_term_ast term ^
+ (match ident with None -> "" | Some id -> " as " ^ id)
+ | DecideEquality _ -> "decide equality"
+ | Decompose (_, term) ->
+ sprintf "decompose %s" (pp_term_ast term)
+ | Discriminate (_, term) -> "discriminate " ^ pp_term_ast term
+ | Elim (_, term, using, num, idents) ->
+ sprintf "elim " ^ pp_term_ast term ^
+ (match using with None -> "" | Some term -> " using " ^ pp_term_ast term)
+ ^ pp_intros_specs (num, idents)
+ | ElimType (_, term, using, num, idents) ->
+ sprintf "elim type " ^ pp_term_ast term ^
+ (match using with None -> "" | Some term -> " using " ^ pp_term_ast term)
+ ^ pp_intros_specs (num, idents)
+ | Exact (_, term) -> "exact " ^ pp_term_ast term
+ | Exists _ -> "exists"
+ | Fold (_, kind, term, pattern) ->
+ sprintf "fold %s %s %s" (pp_reduction_kind kind)
+ (pp_term_ast term) (pp_pattern pattern)
+ | FwdSimpl (_, hyp, idents) ->
+ sprintf "fwd %s%s" hyp
+ (match idents with [] -> "" | idents -> " " ^ pp_idents idents)
+ | Generalize (_, pattern, ident) ->
+ sprintf "generalize %s%s" (pp_pattern pattern)
+ (match ident with None -> "" | Some id -> " as " ^ id)
+ | Goal (_, n) -> "goal " ^ string_of_int n
+ | Fail _ -> "fail"
+ | Fourier _ -> "fourier"
+ | IdTac _ -> "id"
+ | Injection (_, term) -> "injection " ^ pp_term_ast term
+ | Intros (_, None, []) -> "intro"
+ | Intros (_, num, idents) ->
+ sprintf "intros%s%s"
+ (match num with None -> "" | Some num -> " " ^ string_of_int num)
+ (match idents with [] -> "" | idents -> " " ^ pp_idents idents)
+ | LApply (_, level_opt, terms, term, ident_opt) ->
+ sprintf "lapply %s%s%s%s"
+ (match level_opt with None -> "" | Some i -> " depth = " ^ string_of_int i ^ " ")
+ (pp_term_ast term)
+ (match terms with [] -> "" | _ -> " to " ^ pp_terms_ast terms)
+ (match ident_opt with None -> "" | Some ident -> " using " ^ ident)
+ | Left _ -> "left"
+ | LetIn (_, term, ident) -> sprintf "let %s in %s" (pp_term_ast term) ident
+ | Reduce (_, kind, pat) ->
+ sprintf "%s %s" (pp_reduction_kind kind) (pp_pattern pat)
+ | Reflexivity _ -> "reflexivity"
+ | Replace (_, pattern, t) ->
+ sprintf "replace %s with %s" (pp_pattern pattern) (pp_term_ast t)
+ | Rewrite (_, pos, t, pattern) ->
+ sprintf "rewrite %s %s %s"
+ (if pos = `LeftToRight then ">" else "<")
+ (pp_term_ast t)
+ (pp_pattern pattern)
+ | Right _ -> "right"
+ | Ring _ -> "ring"
+ | Split _ -> "split"
+ | Symmetry _ -> "symmetry"
+ | Transitivity (_, term) -> "transitivity " ^ pp_term_ast term
+
+let pp_flavour = function
+ | `Definition -> "Definition"
+ | `Fact -> "Fact"
+ | `Goal -> "Goal"
+ | `Lemma -> "Lemma"
+ | `Remark -> "Remark"
+ | `Theorem -> "Theorem"
+ | `Variant -> "Variant"
+
+let pp_search_kind = function
+ | `Locate -> "locate"
+ | `Hint -> "hint"
+ | `Match -> "match"
+ | `Elim -> "elim"
+ | `Instance -> "instance"
+
+let pp_macro pp_term = function
+ (* Whelp *)
+ | WInstance (_, term) -> "whelp instance " ^ pp_term term
+ | WHint (_, t) -> "whelp hint " ^ pp_term t
+ | WLocate (_, s) -> "whelp locate " ^ s
+ | WElim (_, t) -> "whelp elim " ^ pp_term t
+ | WMatch (_, term) -> "whelp match " ^ pp_term term
+ (* real macros *)
+(* | Abort _ -> "Abort" *)
+ | Check (_, term) -> sprintf "Check %s" (pp_term term)
+ | Hint _ -> "hint"
+(* | Redo (_, None) -> "Redo"
+ | Redo (_, Some n) -> sprintf "Redo %d" n *)
+ | Search_pat (_, kind, pat) ->
+ sprintf "search %s \"%s\"" (pp_search_kind kind) pat
+ | Search_term (_, kind, term) ->
+ sprintf "search %s %s" (pp_search_kind kind) (pp_term term)
+(* | Undo (_, None) -> "Undo"
+ | Undo (_, Some n) -> sprintf "Undo %d" n *)
+ | Print (_, name) -> sprintf "Print \"%s\"" name
+ | Quit _ -> "Quit"
+
+let pp_macro_ast = pp_macro pp_term_ast
+let pp_macro_cic = pp_macro pp_term_cic
+
+let pp_alias = function
+ | Ident_alias (id, uri) -> sprintf "alias id \"%s\" = \"%s\"" id uri
+ | Symbol_alias (symb, instance, desc) ->
+ sprintf "alias symbol \"%s\" (instance %d) = \"%s\""
+ symb instance desc
+ | Number_alias (instance,desc) ->
+ sprintf "alias num (instance %d) = \"%s\"" instance desc
+
+let pp_params = function
+ | [] -> ""
+ | params ->
+ " " ^
+ String.concat " "
+ (List.map
+ (fun (name, typ) -> sprintf "(%s:%s)" name (pp_term_ast typ))
+ params)
+
+let pp_fields fields =
+ (if fields <> [] then "\n" else "") ^
+ String.concat ";\n"
+ (List.map (fun (name,ty) -> " " ^ name ^ ": " ^ pp_term_ast ty) fields)
+
+let pp_obj = function
+ | Inductive (params, types) ->
+ let pp_constructors constructors =
+ String.concat "\n"
+ (List.map (fun (name, typ) -> sprintf "| %s: %s" name (pp_term_ast typ))
+ constructors)
+ in
+ let pp_type (name, _, typ, constructors) =
+ sprintf "\nwith %s: %s \\def\n%s" name (pp_term_ast typ)
+ (pp_constructors constructors)
+ in
+ (match types with
+ | [] -> assert false
+ | (name, inductive, typ, constructors) :: tl ->
+ let fst_typ_pp =
+ sprintf "%sinductive %s%s: %s \\def\n%s"
+ (if inductive then "" else "co") name (pp_params params)
+ (pp_term_ast typ) (pp_constructors constructors)
+ in
+ fst_typ_pp ^ String.concat "" (List.map pp_type tl))
+ | Theorem (flavour, name, typ, body) ->
+ sprintf "%s %s: %s %s"
+ (pp_flavour flavour)
+ name
+ (pp_term_ast typ)
+ (match body with
+ | None -> ""
+ | Some body -> "\\def " ^ pp_term_ast body)
+ | Record (params,name,ty,fields) ->
+ "record " ^ name ^ " " ^ pp_params params ^ " \\def {" ^
+ pp_fields fields ^ "}"
+
+let pp_command = function
+ | Include (_,path) -> "include " ^ path
+ | Qed _ -> "qed"
+ | Drop _ -> "drop"
+ | Set (_, name, value) -> sprintf "set \"%s\" \"%s\"" name value
+ | Coercion (_,term) -> sprintf "coercion %s" (pp_term_ast term)
+ | Alias (_,s) -> pp_alias s
+ | Obj (_,obj) -> pp_obj obj
+ | Default (_,what,uris) ->
+ sprintf "default \"%s\" %s" what
+ (String.concat " " (List.map UriManager.string_of_uri uris))
+
+let rec pp_tactical = function
+ | Tactic (_, tac) -> pp_tactic tac
+ | Do (_, count, tac) -> sprintf "do %d %s" count (pp_tactical tac)
+ | Repeat (_, tac) -> "repeat " ^ pp_tactical tac
+ | Seq (_, tacs) -> pp_tacticals ~sep:"; " tacs
+ | Then (_, tac, tacs) ->
+ sprintf "%s; [%s]" (pp_tactical tac) (pp_tacticals ~sep:" | " tacs)
+ | First (_, tacs) -> sprintf "tries [%s]" (pp_tacticals ~sep:" | " tacs)
+ | Try (_, tac) -> "try " ^ pp_tactical tac
+ | Solve (_, tac) -> sprintf "solve [%s]" (pp_tacticals ~sep:" | " tac)
+
+and pp_tacticals ~sep tacs =
+ String.concat sep (List.map pp_tactical tacs)
+
+let pp_tactical tac = pp_tactical tac ^ tactical_terminator
+let pp_tactic tac = pp_tactic tac ^ tactic_terminator
+let pp_command tac = pp_command tac ^ command_terminator
+
+let pp_executable = function
+ | Macro (_,x) -> pp_macro_ast x
+ | Tactical (_,x) -> pp_tactical x
+ | Command (_,x) -> pp_command x
+
+let pp_comment = function
+ | Note (_,str) -> sprintf "(* %s *)" str
+ | Code (_,code) -> sprintf "(** %s. **)" (pp_executable code)
+
+let pp_statement = function
+ | Executable (_, ex) -> pp_executable ex
+ | Comment (_, c) -> pp_comment c
+
+let pp_cic_command = function
+ | Include (_,path) -> "include " ^ path
+ | Qed _ -> "qed"
+ | Drop _ -> "drop"
+ | Coercion (_,term) -> sprintf "coercion %s" (CicPp.ppterm term)
+ | Set (_, _, _)
+ | Alias (_,_)
+ | Default (_,_,_)
+ | Obj (_,_) -> assert false (* not implemented *)
--- /dev/null
+(* Copyright (C) 2004, 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/
+ *)
+
+val pp_tactic: (CicNotationPt.term, string) GrafiteAst.tactic -> string
+val pp_obj: GrafiteAst.obj -> string
+val pp_command: (CicNotationPt.term,GrafiteAst.obj) GrafiteAst.command -> string
+val pp_macro: ('a -> string) -> 'a GrafiteAst.macro -> string
+val pp_comment: (CicNotationPt.term,GrafiteAst.obj,string) GrafiteAst.comment -> string
+val pp_executable: (CicNotationPt.term,GrafiteAst.obj,string) GrafiteAst.code -> string
+val pp_statement: (CicNotationPt.term,GrafiteAst.obj,string) GrafiteAst.statement -> string
+val pp_macro_ast: CicNotationPt.term GrafiteAst.macro -> string
+val pp_macro_cic: Cic.term GrafiteAst.macro -> string
+val pp_tactical: (CicNotationPt.term, string) GrafiteAst.tactical -> string
+val pp_alias: GrafiteAst.alias_spec -> string
+
+val pp_cic_command: (Cic.term,Cic.obj) GrafiteAst.command -> string
+
let term = CicNotationParser.term
let statement = Grammar.Entry.create grammar "statement"
-let statements = Grammar.Entry.create grammar "statements"
EXTEND
- GLOBAL: term statement statements;
+ GLOBAL: term statement;
arg: [
[ LPAREN; names = LIST1 IDENT SEP SYMBOL ",";
SYMBOL ":"; ty = term; RPAREN -> names,ty
]
];
argument: [
- [ id = IDENT -> GrafiteAst.IdentArg (0, id)
+ [ id = IDENT -> CicNotationPt.IdentArg (0, id)
| l = LIST1 [ SYMBOL <:unicode<eta>> (* η *) -> () ] SEP SYMBOL ".";
SYMBOL "."; id = IDENT ->
- GrafiteAst.IdentArg (List.length l, id)
+ CicNotationPt.IdentArg (List.length l, id)
]
];
associativity: [
]
];
level3_term: [
- [ u = URI -> GrafiteAst.UriPattern (UriManager.uri_of_string u)
- | id = IDENT -> GrafiteAst.VarPattern id
+ [ u = URI -> CicNotationPt.UriPattern (UriManager.uri_of_string u)
+ | id = IDENT -> CicNotationPt.VarPattern id
+ | SYMBOL "_" -> CicNotationPt.ImplicitPattern
| LPAREN; terms = LIST1 SELF; RPAREN ->
(match terms with
| [] -> assert false
| [term] -> term
- | terms -> GrafiteAst.ApplPattern terms)
+ | terms -> CicNotationPt.ApplPattern terms)
]
];
interpretation: [
GrafiteAst.Default (loc,what,uris)
| IDENT "notation"; (l1, assoc, prec, l2) = notation ->
GrafiteAst.Notation (loc, l1, assoc, prec, l2)
- | IDENT "interpretation"; (symbol, args, l3) = interpretation ->
- GrafiteAst.Interpretation (loc, (symbol, args), l3)
+ | IDENT "interpretation"; id = QSTRING;
+ (symbol, args, l3) = interpretation ->
+ GrafiteAst.Interpretation (loc, id, (symbol, args), l3)
| IDENT "dump" -> GrafiteAst.Dump loc
- | IDENT "render"; u = URI -> GrafiteAst.Render (loc, UriManager.uri_of_string u)
+ | IDENT "render"; u = URI ->
+ GrafiteAst.Render (loc, UriManager.uri_of_string u)
]];
executable: [
[ cmd = command; SYMBOL "." -> GrafiteAst.Command (loc, cmd)
statement: [
[ ex = executable -> GrafiteAst.Executable (loc,ex)
| com = comment -> GrafiteAst.Comment (loc, com)
+ | EOI -> raise End_of_file
]
];
- statements: [
- [ l = LIST0 statement ; EOI -> l
- ]
- ];
END
let exc_located_wrapper f =
try
f ()
with
+ | Stdpp.Exc_located (_, End_of_file) -> raise End_of_file
| Stdpp.Exc_located (floc, Stream.Error msg) ->
raise (CicNotationParser.Parse_error (floc, msg))
| Stdpp.Exc_located (floc, exn) ->
let parse_statement stream =
exc_located_wrapper (fun () -> (Grammar.Entry.parse statement stream))
-let parse_statements stream =
- exc_located_wrapper (fun () -> (Grammar.Entry.parse statements stream))
* http://helm.cs.unibo.it/
*)
+ (** @raise End_of_file *)
val parse_statement:
- char Stream.t -> (CicNotationPt.term, GrafiteAst.obj, string) GrafiteAst.statement
-
-val parse_statements:
char Stream.t ->
- (CicNotationPt.term, GrafiteAst.obj, string) GrafiteAst.statement list
+ (CicNotationPt.term, GrafiteAst.obj, string) GrafiteAst.statement
"extending pretty printer took %f)\n")
(time2 -. time1) (time4 -. time3);
flush stdout
- | G.Executable (_, G.Command (_, G.Interpretation (_, l2, l3))) ->
+ | G.Executable (_, G.Command (_, G.Interpretation (_, id, l2, l3))) ->
prerr_endline "Adding interpretation ..."; flush stdout;
let time1 = Unix.gettimeofday () in
- ignore (CicNotationRew.add_interpretation l2 l3);
+ ignore (CicNotationRew.add_interpretation id l2 l3);
let time2 = Unix.gettimeofday () in
printf "done (patterns compilation took %f seconds)\n"
(time2 -. time1);
| `Prop | `CProp -> `Forall
in
idref id (Ast.Binder (binder_kind, (n, Some (aux s)), aux t))
- | Cic.ACast (id,v,t) ->
- idref id (Ast.Appl [idref id (Ast.Symbol ("cast", 0)); aux v; aux t])
+ | Cic.ACast (id,v,t) -> idref id (Ast.Cast (aux v, aux t))
| Cic.ALambda (id,n,s,t) ->
idref id (Ast.Binder (`Lambda, (n, Some (aux s)), aux t))
| Cic.ALetIn (id,n,s,t) -> idref id (Ast.LetIn ((n, None), aux s, aux t))
| Appl of term list
| Binder of binder_kind * capture_variable * term
| Case of term * string option * term option * (case_pattern * term) list
+ | Cast of term * term
| LetIn of capture_variable * term * term
| LetRec of induction_kind * (capture_variable * term * int) list * term
| Ident of string * subst list option
| Binder of binder_kind * capture_variable * term (* kind, name, body *)
| Case of term * string option * term option * (case_pattern * term) list
(* what to match, inductive type, out type, <pattern,action> list *)
+ | Cast of term * term
| LetIn of capture_variable * term * term (* name, body, where *)
| LetRec of induction_kind * (capture_variable * term * int) list * term
(* (name, body, decreasing argument) list, where *)
projects / helm.git / commitdiff