diff options
Diffstat (limited to 'cparser/validator/Interpreter_complete.v')
-rw-r--r-- | cparser/validator/Interpreter_complete.v | 58 |
1 files changed, 29 insertions, 29 deletions
diff --git a/cparser/validator/Interpreter_complete.v b/cparser/validator/Interpreter_complete.v index 3d564c11..eb407061 100644 --- a/cparser/validator/Interpreter_complete.v +++ b/cparser/validator/Interpreter_complete.v @@ -147,16 +147,16 @@ with ptl_zipper: Fixpoint ptlz_cost {hole_symbs hole_word hole_sems} (ptlz:ptl_zipper hole_symbs hole_word hole_sems) := match ptlz with - | Non_terminal_pt_ptlz _ _ _ ptz => + | Non_terminal_pt_ptlz ptz => ptz_cost ptz - | Cons_ptl_ptlz _ _ _ pt _ _ _ ptlz' => + | Cons_ptl_ptlz pt ptlz' => ptlz_cost ptlz' end with ptz_cost {hole_symb hole_word hole_sem} (ptz:pt_zipper hole_symb hole_word hole_sem) := match ptz with | Top_ptz => 0 - | Cons_ptl_ptz _ _ _ _ _ _ ptl ptlz' => + | Cons_ptl_ptz ptl ptlz' => 1 + ptl_size ptl + ptlz_cost ptlz' end. @@ -172,29 +172,29 @@ Inductive pt_dot: Type := Definition ptd_cost (ptd:pt_dot) := match ptd with | Reduce_ptd ptlz => ptlz_cost ptlz - | Shift_ptd _ _ _ _ _ ptl ptlz => 1 + ptl_size ptl + ptlz_cost ptlz + | Shift_ptd _ _ ptl ptlz => 1 + ptl_size ptl + ptlz_cost ptlz end. Fixpoint ptlz_buffer {hole_symbs hole_word hole_sems} (ptlz:ptl_zipper hole_symbs hole_word hole_sems): Stream token := match ptlz with - | Non_terminal_pt_ptlz _ _ _ ptz => + | Non_terminal_pt_ptlz ptz => ptz_buffer ptz - | Cons_ptl_ptlz _ _ _ _ _ _ _ ptlz' => + | Cons_ptl_ptlz _ ptlz' => ptlz_buffer ptlz' end with ptz_buffer {hole_symb hole_word hole_sem} (ptz:pt_zipper hole_symb hole_word hole_sem): Stream token := match ptz with | Top_ptz => buffer_end - | Cons_ptl_ptz _ _ _ _ wordq _ ptl ptlz' => + | @Cons_ptl_ptz _ _ _ _ wordq _ ptl ptlz' => wordq++ptlz_buffer ptlz' end. Definition ptd_buffer (ptd:pt_dot) := match ptd with | Reduce_ptd ptlz => ptlz_buffer ptlz - | Shift_ptd term sem _ wordq _ _ ptlz => + | @Shift_ptd term sem _ wordq _ _ ptlz => Cons (existT (fun t => symbol_semantic_type (T t)) term sem) (wordq ++ ptlz_buffer ptlz) end. @@ -202,16 +202,16 @@ Definition ptd_buffer (ptd:pt_dot) := Fixpoint ptlz_prod {hole_symbs hole_word hole_sems} (ptlz:ptl_zipper hole_symbs hole_word hole_sems): production := match ptlz with - | Non_terminal_pt_ptlz prod _ _ _ => prod - | Cons_ptl_ptlz _ _ _ _ _ _ _ ptlz' => + | @Non_terminal_pt_ptlz prod _ _ _ => prod + | Cons_ptl_ptlz _ ptlz' => ptlz_prod ptlz' end. Fixpoint ptlz_past {hole_symbs hole_word hole_sems} (ptlz:ptl_zipper hole_symbs hole_word hole_sems): list symbol := match ptlz with - | Non_terminal_pt_ptlz _ _ _ _ => [] - | Cons_ptl_ptlz s _ _ _ _ _ _ ptlz' => s::ptlz_past ptlz' + | Non_terminal_pt_ptlz _ => [] + | @Cons_ptl_ptlz s _ _ _ _ _ _ ptlz' => s::ptlz_past ptlz' end. Lemma ptlz_past_ptlz_prod: @@ -236,12 +236,12 @@ Fixpoint ptlz_stack_compat {hole_symbs hole_word hole_sems} (stack:stack): Prop := ptlz_state_compat ptlz (state_of_stack init stack) /\ match ptlz with - | Non_terminal_pt_ptlz _ _ _ ptz => + | Non_terminal_pt_ptlz ptz => ptz_stack_compat ptz stack - | Cons_ptl_ptlz _ _ sem _ _ _ _ ptlz' => + | @Cons_ptl_ptlz _ _ sem _ _ _ _ ptlz' => match stack with | [] => False - | existT _ sem'::stackq => + | existT _ _ sem'::stackq => ptlz_stack_compat ptlz' stackq /\ sem ~= sem' end @@ -251,7 +251,7 @@ with ptz_stack_compat {hole_symb hole_word hole_sem} (stack:stack): Prop := match ptz with | Top_ptz => stack = [] - | Cons_ptl_ptz _ _ _ _ _ _ _ ptlz' => + | Cons_ptl_ptz _ ptlz' => ptlz_stack_compat ptlz' stack end. @@ -267,7 +267,7 @@ Qed. Definition ptd_stack_compat (ptd:pt_dot) (stack:stack): Prop := match ptd with | Reduce_ptd ptlz => ptlz_stack_compat ptlz stack - | Shift_ptd _ _ _ _ _ _ ptlz => ptlz_stack_compat ptlz stack + | Shift_ptd _ _ _ ptlz => ptlz_stack_compat ptlz stack end. Fixpoint build_pt_dot {hole_symbs hole_word hole_sems} @@ -279,13 +279,13 @@ Fixpoint build_pt_dot {hole_symbs hole_word hole_sems} with | Nil_ptl => fun ptlz => Reduce_ptd ptlz - | Cons_ptl _ _ _ pt _ _ _ ptl' => + | Cons_ptl pt ptl' => match pt in parse_tree hole_symb hole_word hole_sem return ptl_zipper (hole_symb::_) (hole_word++_) (hole_sem,_) -> _ with | Terminal_pt term sem => fun ptlz => Shift_ptd term sem ptl' ptlz - | Non_terminal_pt _ _ _ ptl'' => fun ptlz => + | Non_terminal_pt ptl'' => fun ptlz => build_pt_dot ptl'' (Non_terminal_pt_ptlz (Cons_ptl_ptz ptl' ptlz)) end @@ -360,10 +360,10 @@ Program Fixpoint pop_ptlz {hole_symbs hole_word hole_sems} (pt_zipper (NT (prod_lhs (ptlz_prod ptlz))) word sem * parse_tree (NT (prod_lhs (ptlz_prod ptlz))) word sem)%type } } with - | Non_terminal_pt_ptlz prod word sem ptz => fun ptl => + | @Non_terminal_pt_ptlz prod word sem ptz => fun ptl => let sem := uncurry (prod_action prod) sem in existT _ word (existT _ sem (ptz, Non_terminal_pt ptl)) - | Cons_ptl_ptlz _ _ _ pt _ _ _ ptlz' => fun ptl => + | Cons_ptl_ptlz pt ptlz' => fun ptl => pop_ptlz (Cons_ptl pt ptl) ptlz' end ptl. @@ -371,7 +371,7 @@ Lemma pop_ptlz_cost: forall hole_symbs hole_word hole_sems (ptl:parse_tree_list hole_symbs hole_word hole_sems) (ptlz:ptl_zipper hole_symbs hole_word hole_sems), - let 'existT word (existT sem (ptz, pt)) := pop_ptlz ptl ptlz in + let 'existT _ word (existT _ sem (ptz, pt)) := pop_ptlz ptl ptlz in ptlz_cost ptlz = ptz_cost ptz. Proof. fix 5. @@ -384,7 +384,7 @@ Lemma pop_ptlz_buffer: forall hole_symbs hole_word hole_sems (ptl:parse_tree_list hole_symbs hole_word hole_sems) (ptlz:ptl_zipper hole_symbs hole_word hole_sems), - let 'existT word (existT sem (ptz, pt)) := pop_ptlz ptl ptlz in + let 'existT _ word (existT _ sem (ptz, pt)) := pop_ptlz ptl ptlz in ptlz_buffer ptlz = ptz_buffer ptz. Proof. fix 5. @@ -419,7 +419,7 @@ Lemma pop_ptlz_pop_stack_compat: eq_rect _ (fun x=>x) (prod_action (ptlz_prod ptlz)) _ (pop_ptlz_pop_stack_compat_converter _ _ _ _ _) in - let 'existT word (existT sem (ptz, pt)) := pop_ptlz ptl ptlz in + let 'existT _ word (existT _ sem (ptz, pt)) := pop_ptlz ptl ptlz in match pop (ptlz_past ptlz) stack (uncurry action' hole_sems) with | OK (stack', sem') => ptz_stack_compat ptz stack' /\ sem = sem' @@ -431,7 +431,7 @@ fix 5. destruct ptlz. intros; simpl. split. apply H. -f_equal. +eapply (f_equal (fun X => uncurry X semantic_values)). apply JMeq_eq, JMeq_sym, JMeq_eqrect with (P:=fun x => x). simpl; intros; destruct stack0. destruct (proj2 H). @@ -451,13 +451,13 @@ Qed. Definition next_ptd (ptd:pt_dot): option pt_dot := match ptd with - | Shift_ptd term sem _ _ _ ptl ptlz => + | Shift_ptd term sem ptl ptlz => Some (build_pt_dot ptl (Cons_ptl_ptlz (Terminal_pt term sem) ptlz)) | Reduce_ptd ptlz => - let 'existT _ (existT _ (ptz, pt)) := pop_ptlz Nil_ptl ptlz in + let 'existT _ _ (existT _ _ (ptz, pt)) := pop_ptlz Nil_ptl ptlz in match ptz in pt_zipper sym _ _ return parse_tree sym _ _ -> _ with | Top_ptz => fun pt => None - | Cons_ptl_ptz _ _ _ _ _ _ ptl ptlz' => + | Cons_ptl_ptz ptl ptlz' => fun pt => Some (build_pt_dot ptl (Cons_ptl_ptlz pt ptlz')) end pt end. @@ -615,7 +615,7 @@ Definition init_ptd := match head return Type with | T _ => unit | NT _ => pt_dot end with | Terminal_pt _ _ => fun _ => () - | Non_terminal_pt _ _ _ ptl => + | Non_terminal_pt ptl => fun top => build_pt_dot ptl (Non_terminal_pt_ptlz top) end Top_ptz. |