X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_procedural%2FproceduralTypes.ml;h=3b6afc4c31ac0d54f18d58613c583311801e199d;hb=ff3bd23d19abd7c9e981fd754f54d536fc563ec3;hp=2d3c915f7234e7ed8b7437086277ec4d77740d85;hpb=cf4301b669442bdd78984d3a3a1e38660db1f2ea;p=helm.git diff --git a/helm/software/components/acic_procedural/proceduralTypes.ml b/helm/software/components/acic_procedural/proceduralTypes.ml index 2d3c915f7..3b6afc4c3 100644 --- a/helm/software/components/acic_procedural/proceduralTypes.ml +++ b/helm/software/components/acic_procedural/proceduralTypes.ml @@ -54,19 +54,24 @@ let list_init f i = (****************************************************************************) +type flavour = C.object_flavour type name = string option type hyp = string -type what = Cic.annterm +type what = C.annterm type how = bool -type using = Cic.annterm +type using = C.annterm type count = int type note = string type where = (hyp * name) option -type inferred = Cic.annterm -type pattern = Cic.annterm +type inferred = C.annterm +type pattern = C.annterm +type body = C.annterm option +type types = C.anninductiveType list +type lpsno = int type step = Note of note - | Theorem of name * what * note + | Inductive of types * lpsno * note + | Statement of flavour * name * what * body * note | Qed of note | Id of note | Intros of count option * name list * note @@ -74,6 +79,7 @@ type step = Note of note | LetIn of name * what * note | Rewrite of how * what * where * pattern * note | Elim of what * using option * pattern * note + | Cases of what * pattern * note | Apply of what * note | Change of inferred * what * where * pattern * note | Clear of hyp list * note @@ -82,7 +88,34 @@ type step = Note of note (* annterm constructors *****************************************************) -let mk_arel i b = Cic.ARel ("", "", i, b) +let mk_arel i b = C.ARel ("", "", i, b) + +(* FG: this is really awful !! *) +let arel_of_name = function + | C.Name s -> mk_arel 0 s + | C.Anonymous -> mk_arel 0 "_" + +(* helper functions on left params for use with inductive types *************) + +let strip_lps lpsno arity = + let rec aux no lps = function + | C.AProd (_, name, w, t) when no > 0 -> + let lp = name, Some w in + aux (pred no) (lp :: lps) t + | t -> lps, t + in + aux lpsno [] arity + +let merge_lps lps1 lps2 = + let map (n1, w1) (n2, _) = + let n = match n1, n2 with + | C.Name _, _ -> n1 + | _ -> n2 + in + n, w1 + in + if lps1 = [] then lps2 else + List.map2 map lps1 lps2 (* grafite ast constructors *************************************************) @@ -99,9 +132,25 @@ let mk_notenote str a = let mk_thnote str a = if str = "" then a else mk_note "" :: mk_note str :: a -let mk_theorem name t = +let mk_inductive types lpsno = + let map1 (lps1, cons) (name, arity) = + let lps2, arity = strip_lps lpsno arity in + merge_lps lps1 lps2, (name, arity) :: cons + in + let map2 (lps1, types) (_, name, kind, arity, cons) = + let lps2, arity = strip_lps lpsno arity in + let lps1, rev_cons = List.fold_left map1 (lps1, []) cons in + merge_lps lps1 lps2, (name, kind, arity, List.rev rev_cons) :: types + in + let map3 (name, xw) = arel_of_name name, xw in + let rev_lps, rev_types = List.fold_left map2 ([], []) types in + let lpars, types = List.rev_map map3 rev_lps, List.rev rev_types in + let obj = N.Inductive (lpars, types) in + G.Executable (floc, G.Command (floc, G.Obj (floc, obj))) + +let mk_statement flavour name t v = let name = match name with Some name -> name | None -> assert false in - let obj = N.Theorem (`Theorem, name, t, None) in + let obj = N.Theorem (flavour, name, t, v) in G.Executable (floc, G.Command (floc, G.Obj (floc, obj))) let mk_qed = @@ -134,8 +183,9 @@ let mk_letin name what punctation = let mk_rewrite direction what where pattern punctation = let direction = if direction then `RightToLeft else `LeftToRight in let pattern, rename = match where with - | None -> (None, [], Some pattern), [] - | Some (premise, name) -> (None, [premise, pattern], None), [name] + | None -> (None, [], Some pattern), [] + | Some (premise, Some name) -> (None, [premise, pattern], None), [Some name] + | Some (premise, None) -> (None, [premise, pattern], None), [] in let tactic = G.Rewrite (floc, direction, what, pattern, rename) in mk_tactic tactic punctation @@ -145,8 +195,13 @@ let mk_elim what using pattern punctation = let tactic = G.Elim (floc, what, using, pattern, (Some 0, [])) in mk_tactic tactic punctation +let mk_cases what pattern punctation = + let pattern = None, [], Some pattern in + let tactic = G.Cases (floc, what, pattern, (Some 0, [])) in + mk_tactic tactic punctation + let mk_apply t punctation = - let tactic = G.Apply (floc, t) in + let tactic = G.ApplyP (floc, t) in mk_tactic tactic punctation let mk_change t where pattern punctation = @@ -180,22 +235,24 @@ let mk_vb = G.Shift floc (* rendering ****************************************************************) let rec render_step sep a = function - | Note s -> mk_notenote s a - | Theorem (n, t, s) -> mk_theorem n t :: mk_thnote s a - | Qed s -> mk_qed :: mk_tacnote s a - | Id s -> mk_id sep :: mk_tacnote s a - | Intros (c, ns, s) -> mk_intros c ns sep :: mk_tacnote s a - | Cut (n, t, s) -> mk_cut n t sep :: mk_tacnote s a - | LetIn (n, t, s) -> mk_letin n t sep :: mk_tacnote s a - | Rewrite (b, t, w, e, s) -> mk_rewrite b t w e sep :: mk_tacnote s a - | Elim (t, xu, e, s) -> mk_elim t xu e sep :: mk_tacnote s a - | Apply (t, s) -> mk_apply t sep :: mk_tacnote s a - | Change (t, _, w, e, s) -> mk_change t w e sep :: mk_tacnote s a - | Clear (ns, s) -> mk_clear ns sep :: mk_tacnote s a - | ClearBody (n, s) -> mk_clearbody n sep :: mk_tacnote s a - | Branch ([], s) -> a - | Branch ([ps], s) -> render_steps sep a ps - | Branch (ps :: pss, s) -> + | Note s -> mk_notenote s a + | Statement (f, n, t, v, s) -> mk_statement f n t v :: mk_thnote s a + | Inductive (lps, ts, s) -> mk_inductive lps ts :: mk_thnote s a + | Qed s -> mk_qed :: mk_tacnote s a + | Id s -> mk_id sep :: mk_tacnote s a + | Intros (c, ns, s) -> mk_intros c ns sep :: mk_tacnote s a + | Cut (n, t, s) -> mk_cut n t sep :: mk_tacnote s a + | LetIn (n, t, s) -> mk_letin n t sep :: mk_tacnote s a + | Rewrite (b, t, w, e, s) -> mk_rewrite b t w e sep :: mk_tacnote s a + | Elim (t, xu, e, s) -> mk_elim t xu e sep :: mk_tacnote s a + | Cases (t, e, s) -> mk_cases t e sep :: mk_tacnote s a + | Apply (t, s) -> mk_apply t sep :: mk_tacnote s a + | Change (t, _, w, e, s) -> mk_change t w e sep :: mk_tacnote s a + | Clear (ns, s) -> mk_clear ns sep :: mk_tacnote s a + | ClearBody (n, s) -> mk_clearbody n sep :: mk_tacnote s a + | Branch ([], s) -> a + | Branch ([ps], s) -> render_steps sep a ps + | Branch (ps :: pss, s) -> let a = mk_ob :: mk_tacnote s a in let a = List.fold_left (render_steps mk_vb) a (List.rev pss) in mk_punctation sep :: render_steps mk_cb a ps @@ -208,7 +265,7 @@ and render_steps sep a = function | p :: ((Branch (_ :: _ :: _, _) :: _) as ps) -> render_steps sep (render_step mk_sc a p) ps | p :: ps -> - render_steps sep (render_step mk_dot a p) ps + render_steps sep (render_step mk_sc a p) ps let render_steps a = render_steps mk_dot a @@ -216,7 +273,7 @@ let render_steps a = render_steps mk_dot a let rec count_step a = function | Note _ - | Theorem _ + | Statement _ | Qed _ -> a | Branch (pps, _) -> List.fold_left count_steps a pps | _ -> succ a @@ -225,7 +282,8 @@ and count_steps a = List.fold_left count_step a let rec count_node a = function | Note _ - | Theorem _ + | Inductive _ + | Statement _ | Qed _ | Id _ | Intros _ @@ -236,6 +294,7 @@ let rec count_node a = function | Apply (t, _) -> I.count_nodes a (H.cic t) | Rewrite (_, t, _, p, _) | Elim (t, _, p, _) + | Cases (t, p, _) | Change (t, _, _, p, _) -> let a = I.count_nodes a (H.cic t) in I.count_nodes a (H.cic p)