From: Stefano Zacchiroli Date: Wed, 8 Jun 2005 07:41:51 +0000 (+0000) Subject: snapshot (minor changes) X-Git-Tag: PRE_INDEX_1~45 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ec54d490477ece51c19d79750dda9805ffda663c;p=helm.git snapshot (minor changes) --- diff --git a/helm/ocaml/cic_notation/.depend b/helm/ocaml/cic_notation/.depend index cd8873184..6b0466b69 100644 --- a/helm/ocaml/cic_notation/.depend +++ b/helm/ocaml/cic_notation/.depend @@ -12,14 +12,16 @@ cicNotationTag.cmo: cicNotationUtil.cmi cicNotationPt.cmo cicNotationTag.cmi 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 \ @@ -28,7 +30,9 @@ 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: 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 diff --git a/helm/ocaml/cic_notation/TODO b/helm/ocaml/cic_notation/TODO index 0d45846e5..b7e910e68 100644 --- a/helm/ocaml/cic_notation/TODO +++ b/helm/ocaml/cic_notation/TODO @@ -15,6 +15,7 @@ TODO - 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 diff --git a/helm/ocaml/cic_notation/cicNotationParser.ml b/helm/ocaml/cic_notation/cicNotationParser.ml index 246417d77..6bc494cdc 100644 --- a/helm/ocaml/cic_notation/cicNotationParser.ml +++ b/helm/ocaml/cic_notation/cicNotationParser.ml @@ -244,10 +244,6 @@ let delete atoms = Grammar.delete_rule l2_pattern atoms (** {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 @@ -329,7 +325,7 @@ EXTEND 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))) ] diff --git a/helm/ocaml/cic_notation/cicNotationRew.ml b/helm/ocaml/cic_notation/cicNotationRew.ml index 529353daa..151ec8a08 100644 --- a/helm/ocaml/cic_notation/cicNotationRew.ml +++ b/helm/ocaml/cic_notation/cicNotationRew.ml @@ -223,12 +223,8 @@ let set_compiled32 f = compiled32 := Some f 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 -> @@ -264,12 +260,14 @@ let instantiate21 env precedence associativity l1 = | [] -> 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 = diff --git a/helm/ocaml/cic_notation/cicNotationUtil.ml b/helm/ocaml/cic_notation/cicNotationUtil.ml index 52ac0ab67..e09ac345b 100644 --- a/helm/ocaml/cic_notation/cicNotationUtil.ml +++ b/helm/ocaml/cic_notation/cicNotationUtil.ml @@ -307,3 +307,7 @@ let string_of_literal = function | `Keyword s | `Number s -> s +let boxify = function + | [ a ] -> a + | l -> Layout (Box (H, l)) + diff --git a/helm/ocaml/cic_notation/cicNotationUtil.mli b/helm/ocaml/cic_notation/cicNotationUtil.mli index 760d95ae9..f35fbb3d3 100644 --- a/helm/ocaml/cic_notation/cicNotationUtil.mli +++ b/helm/ocaml/cic_notation/cicNotationUtil.mli @@ -46,3 +46,5 @@ val ncombine: 'a list list -> 'a list list val string_of_literal: CicNotationPt.literal -> string +val boxify: CicNotationPt.term list -> CicNotationPt.term + diff --git a/helm/ocaml/cic_notation/doc/samples.ma b/helm/ocaml/cic_notation/doc/samples.ma new file mode 100644 index 000000000..f0a75667c --- /dev/null +++ b/helm/ocaml/cic_notation/doc/samples.ma @@ -0,0 +1,45 @@ +# 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 \]. + diff --git a/helm/ocaml/cic_notation/test_parser.ml b/helm/ocaml/cic_notation/test_parser.ml index 98716ad86..58880b9d5 100644 --- a/helm/ocaml/cic_notation/test_parser.ml +++ b/helm/ocaml/cic_notation/test_parser.ml @@ -35,40 +35,6 @@ let _ = 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;