cicNotationTag.cmx: cicNotationUtil.cmx cicNotationPt.cmx cicNotationTag.cmi
cicNotationLexer.cmo: cicNotationLexer.cmi
cicNotationLexer.cmx: cicNotationLexer.cmi
-cicNotationEnv.cmo: cicNotationPt.cmo cicNotationEnv.cmi
-cicNotationEnv.cmx: cicNotationPt.cmx cicNotationEnv.cmi
+cicNotationEnv.cmo: cicNotationUtil.cmi cicNotationPt.cmo cicNotationEnv.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: cicNotationUtil.cmi cicNotationTag.cmi \
- cicNotationPt.cmo cicNotationEnv.cmi cicNotationMatcher.cmi
+ cicNotationPt.cmo cicNotationPp.cmi cicNotationEnv.cmi \
+ cicNotationMatcher.cmi
cicNotationMatcher.cmx: cicNotationUtil.cmx cicNotationTag.cmx \
- cicNotationPt.cmx cicNotationEnv.cmx cicNotationMatcher.cmi
+ 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 \
cicNotationMatcher.cmi cicNotationEnv.cmi cicNotationRew.cmi
cicNotationRew.cmx: cicNotationUtil.cmx cicNotationPt.cmx \
cicNotationMatcher.cmx cicNotationEnv.cmx cicNotationRew.cmi
-cicNotationParser.cmo: cicNotationPt.cmo cicNotationPp.cmi \
- cicNotationLexer.cmi cicNotationEnv.cmi cicNotationParser.cmi
-cicNotationParser.cmx: cicNotationPt.cmx cicNotationPp.cmx \
- cicNotationLexer.cmx cicNotationEnv.cmx cicNotationParser.cmi
+cicNotationParser.cmo: cicNotationUtil.cmi cicNotationPt.cmo \
+ cicNotationPp.cmi cicNotationLexer.cmi cicNotationEnv.cmi \
+ cicNotationParser.cmi
+cicNotationParser.cmx: cicNotationUtil.cmx cicNotationPt.cmx \
+ cicNotationPp.cmx cicNotationLexer.cmx cicNotationEnv.cmx \
+ cicNotationParser.cmi
- studiare/implementare sintassi con ... per i magic fold
* integrazione
- porting della disambiguazione al nuovo ast
+ - apportare all'ast le modifiche di CicAst (cast, case)
DONE
(** {2 Grammar} *)
-let boxify = function
- | [ a ] -> a
- | l -> Layout (Box (H, l))
-
let fold_binder binder pt_names body =
let fold_cluster binder terms ty body =
List.fold_right
return_term loc (Layout (Box (V, p)))
| SYMBOL "\\BREAK" -> return_term loc (Layout Break)
| DELIM "\\["; p = l1_pattern; DELIM "\\]" ->
- return_term loc (boxify p)
+ return_term loc (CicNotationUtil.boxify p)
| p = SELF; SYMBOL "\\AS"; id = IDENT ->
return_term loc (Variable (Ascription (p, id)))
]
let instantiate21 env precedence associativity l1 =
prerr_endline "instantiate21";
- let boxify = function
- | [t] -> t
- | tl -> Ast.Layout (Ast.Box (Ast.H, tl))
- in
let rec subst_singleton env t =
- boxify (subst env t)
+ CicNotationUtil.boxify (subst env t)
and subst env = function
| Ast.AttributedTerm (_, t) -> subst env t
| Ast.Variable var ->
| [] -> List.rev acc
| value_set :: [] ->
let env = CicNotationEnv.combine rec_decls value_set in
- instantiate_list ((boxify (subst env p)) :: acc) []
+ instantiate_list
+ ((CicNotationUtil.boxify (subst env p)) :: acc) []
| value_set :: tl ->
let env = CicNotationEnv.combine rec_decls value_set in
- instantiate_list ((boxify (subst env p @ sep)) :: acc) tl
+ instantiate_list
+ ((CicNotationUtil.boxify (subst env p @ sep)) :: acc) tl
in
- instantiate_list [] (List.rev values)
+ instantiate_list [] values
| Ast.Opt p ->
let opt_decls = CicNotationEnv.declarations_of_term p in
let env =
| `Keyword s
| `Number s -> s
+let boxify = function
+ | [ a ] -> a
+ | l -> Layout (Box (H, l))
+
val string_of_literal: CicNotationPt.literal -> string
+val boxify: CicNotationPt.term list -> CicNotationPt.term
+
--- /dev/null
+# sample mappings level 1 <--> level 2
+
+notation \[ \TERM a ++ \OPT \NUM i \] for 'assign \TERM a ('plus \TERM a \DEFAULT \[\NUM i\] \[1\]).
+print 1 ++ 2.
+
+notation \[ + \LIST0 \NUM a \] for \FOLD right \[ 'zero \] \LAMBDA acc \[ 'plus \NUM a \TERM acc \].
+print + 1 2 3 4.
+
+notation \[ [ \LIST0 \TERM a \SEP ; ] \] for \FOLD right \[ 'nil \] \LAMBDA acc \[ 'cons \TERM a \TERM acc \].
+print [].
+print [1;2;3;4].
+
+notation \[ [ \LIST0 \[ \TERM a ; \TERM b \] \SEP ; ] \] for \FOLD right \[ 'nil \] \LAMBDA acc \[ 'cons \TERM a ( 'cons \TERM b \TERM acc) \] .
+print [].
+print [1;2].
+print [1;2;3;4].
+
+notation \[ | \LIST0 \[ \TERM a \OPT \[ , \TERM b \] \] \SEP ; | \] for \FOLD right \[ 'nil \] \LAMBDA acc \[ 'cons \DEFAULT \[ \TERM a \] \[ ('pair \TERM a \TERM b) \] \TERM acc \] .
+
+notation \[ | \LIST0 \[ \OPT \[ \NUM i \] \] \SEP ; | \] for \FOLD right \[ 'nil \] \LAMBDA acc \[ 'cons \DEFAULT \[ 'Some \NUM i \] \[ 'None \] \TERM acc \] .
+
+# sample mappings level 2 <--> level 3
+
+interpretation 'plus x y = (cic:/Coq/Init/Peano/plus.con x y).
+interpretation 'mult x y = (cic:/Coq/Init/Peano/mult.con x y).
+render cic:/Coq/Arith/Mult/mult_plus_distr_r.con.
+
+interpretation 'megacoso x y z w = (cic:/Coq/Init/Logic/eq.ind#xpointer(1/1) cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1) (cic:/Coq/Init/Peano/plus.con x y) (cic:/Coq/Init/Peano/plus.con z w)).
+render cic:/Coq/Arith/Plus/plus_comm.con.
+
+# full samples
+
+notation \[ \TERM a + \TERM b \] for 'plus \TERM a \TERM b.
+print 1 + 2.
+interpretation 'plus x y = (cic:/Coq/Init/Peano/plus.con x y).
+render cic:/Coq/Arith/Plus/plus_comm.con.
+
+notation \[ \TERM a + \TERM b \] for 'plus \TERM a \TERM b.
+notation \[ \TERM a * \TERM b \] for 'mult \TERM a \TERM b.
+interpretation 'plus x y = (cic:/Coq/Init/Peano/plus.con x y).
+interpretation 'mult x y = (cic:/Coq/Init/Peano/mult.con x y).
+render cic:/Coq/Arith/Mult/mult_plus_distr_r.con.
+
+notation \[ \LIST \NUM a \] for \FOLD left \[ 'a \] \LAMBDA acc \[ 'b \NUM a \].
+
let arg_spec = [ "-level", Arg.Set_int level, "set the notation level" ] in
let usage = "test_parser -level { 1 | 2 | 3 }" in
Arg.parse arg_spec (fun _ -> raise (Arg.Bad usage)) usage;
- if !level = 2 then begin
- let id =
- CicNotationParser.extend ~precedence:50 ~associativity:Gramext.LeftA
- (P.Layout (P.Box (P.H,
- [
- P.Magic
- (P.List1
- (P.Layout (P.Box (P.H,
- [ P.Literal (`Symbol "|");
- P.Variable (P.TermVar "ugo");
- P.Magic (P.Opt (P.Layout (P.Box (P.H,
- [ P.Literal (`Symbol ",");
- P.Variable (P.TermVar "pino")]))));
- P.Literal (`Symbol "|");
- ])),
- Some (`Symbol ";")));
-(* P.Literal (`Symbol "+");
- P.Magic (P.Opt (P.Layout (P.Box (P.H,
- [
- P.Variable (P.TermVar "ugo");
- P.Literal (`Symbol "+");
- P.Variable (P.TermVar "pino")
- ])))); *)
-(* P.Variable (P.TermVar "a");
- P.Literal (`Symbol "+");
- P.Variable (P.TermVar "b"); *)
- ])))
- (fun env _ ->
- prerr_endline "reducing rule" ;
- prerr_endline (sprintf "env = [ %s ]" (CicNotationPp.pp_env env));
- P.Sort `Prop)
- in
- CicNotationParser.print_l2_pattern ()
- end;
let ic = stdin in
try
printf "Parsing notation level %d\n" !level; flush stdout;
projects / helm.git / commitdiff