From: Stefano Zacchiroli Date: Thu, 2 Jun 2005 19:56:57 +0000 (+0000) Subject: snapshot (added typed environment in 2 -> 1 conversion) X-Git-Tag: PRE_INDEX_1~73 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ea6b99ed26a954a578e3c88909479dcf9cab7345;p=helm.git snapshot (added typed environment in 2 -> 1 conversion) ... in the eye of the meta-vortex ... ... from Ravenna city --- diff --git a/helm/ocaml/cic_notation/cicNotationEnv.ml b/helm/ocaml/cic_notation/cicNotationEnv.ml index 13920157e..b6ae4e6be 100644 --- a/helm/ocaml/cic_notation/cicNotationEnv.ml +++ b/helm/ocaml/cic_notation/cicNotationEnv.ml @@ -72,3 +72,31 @@ let list_binding_of_name (n, ty) = (n, (ListType ty, ListValue [])) let opt_declaration (n, ty) = (n, OptType ty) let list_declaration (n, ty) = (n, ListType ty) +let declaration_of_var = function + | NumVar s -> s, NumType + | IdentVar s -> s, StringType + | TermVar s -> s, TermType + | _ -> assert false + +let value_of_term = function + | Num (s, _) -> NumValue s + | Ident (s, None) -> StringValue s + | t -> TermValue t + +let term_of_value = function + | NumValue s -> Num (s, 0) + | StringValue s -> Ident (s, None) + | TermValue t -> t + | _ -> assert false (* TO BE UNDERSTOOD *) + +let rec well_typed ty value = + match ty, value with + | TermType, TermValue _ + | StringType, StringValue _ + | OptType _, OptValue None + | NumType, NumValue _ -> true + | OptType ty', OptValue (Some value') -> well_typed ty' value' + | ListType ty', ListValue vl -> + List.for_all (fun value' -> well_typed ty' value') vl + | _ -> false + diff --git a/helm/ocaml/cic_notation/cicNotationEnv.mli b/helm/ocaml/cic_notation/cicNotationEnv.mli index 3059fc098..877a16f52 100644 --- a/helm/ocaml/cic_notation/cicNotationEnv.mli +++ b/helm/ocaml/cic_notation/cicNotationEnv.mli @@ -45,6 +45,11 @@ type declaration = string * value_type type binding = string * (value_type * value) type t = binding list +val declaration_of_var: CicNotationPt.pattern_variable -> declaration +val value_of_term: CicNotationPt.term -> value +val term_of_value: value -> CicNotationPt.term +val well_typed: value_type -> value -> bool + (** {2 Environment lookup} *) val lookup_value: t -> string -> value diff --git a/helm/ocaml/cic_notation/cicNotationParser.ml b/helm/ocaml/cic_notation/cicNotationParser.ml index 767aa3d15..fa8b65ed0 100644 --- a/helm/ocaml/cic_notation/cicNotationParser.ml +++ b/helm/ocaml/cic_notation/cicNotationParser.ml @@ -85,34 +85,34 @@ let make_action action bindings = | NoBinding :: tl -> prerr_endline "aux: none"; Gramext.action (fun _ -> aux vl tl) - (* LUCA: DEFCON 2 BEGIN *) + (* LUCA: DEFCON 5 BEGIN *) | Binding (name, TermType) :: tl -> prerr_endline "aux: term"; Gramext.action - (fun (v:term) -> aux ((name, (TermType, (TermValue v)))::vl) tl) + (fun (v:term) -> aux ((name, (TermType, TermValue v))::vl) tl) | Binding (name, StringType) :: tl -> prerr_endline "aux: string"; Gramext.action (fun (v:string) -> - aux ((name, (StringType, (StringValue v))) :: vl) tl) + aux ((name, (StringType, StringValue v)) :: vl) tl) | Binding (name, NumType) :: tl -> prerr_endline "aux: num"; Gramext.action - (fun (v:string) -> aux ((name, (NumType, (NumValue v))) :: vl) tl) + (fun (v:string) -> aux ((name, (NumType, NumValue v)) :: vl) tl) | Binding (name, OptType t) :: tl -> prerr_endline "aux: opt"; Gramext.action (fun (v:'a option) -> - aux ((name, (OptType t, (OptValue v))) :: vl) tl) + aux ((name, (OptType t, OptValue v)) :: vl) tl) | Binding (name, ListType t) :: tl -> prerr_endline "aux: list"; Gramext.action (fun (v:'a list) -> - aux ((name, (ListType t, (ListValue v))) :: vl) tl) + aux ((name, (ListType t, ListValue v)) :: vl) tl) | Env _ :: tl -> prerr_endline "aux: env"; Gramext.action (fun (v:CicNotationEnv.t) -> aux (v @ vl) tl) - (* LUCA: DEFCON 2 END *) + (* LUCA: DEFCON 5 END *) in aux [] (List.rev bindings) diff --git a/helm/ocaml/cic_notation/cicNotationRew.ml b/helm/ocaml/cic_notation/cicNotationRew.ml index e037ca2a9..7dd973989 100644 --- a/helm/ocaml/cic_notation/cicNotationRew.ml +++ b/helm/ocaml/cic_notation/cicNotationRew.ml @@ -85,12 +85,12 @@ module Patterns (P: PATTERN) = (* return 2 lists of rows, first one containing homogeneous rows according * to "compatible" below *) let horizontal_split t = - let ap = + let ap, first_row, t' = match t with | [] -> assert false | ([], _) :: _ -> assert false (* are_empty should have been invoked in advance *) - | (hd :: _ , _) :: _ -> hd + | ((hd :: _ , _) as row) :: tl -> hd, row, tl in let rec aux prev_t = function | [] -> List.rev prev_t, [] @@ -99,7 +99,7 @@ module Patterns (P: PATTERN) = aux (row :: prev_t) tl | t -> List.rev prev_t, t in - aux [] t + aux [first_row] t' (* return 2 lists, first one representing first column, second one * representing rows stripped of the first element *) @@ -561,7 +561,10 @@ let variable_closure21 vars k = match terms with | hd :: tl -> let envl' = - List.map2 (fun var (env, pid) -> (var, hd) :: env, pid) vars envl + List.map2 + (fun (name, ty) (env, pid) -> + (name, (ty, CicNotationEnv.value_of_term hd)) :: env, pid) + vars envl in k tl envl' | _ -> assert false) @@ -602,7 +605,7 @@ let compiler21 (t: Patterns21.t) success_k fail_k = let vars = List.map (function - | Ast.Variable v -> v + | Ast.Variable v -> CicNotationEnv.declaration_of_var v | _ -> assert false) first_column in @@ -654,9 +657,19 @@ let instantiate21 env pid = let rec subst = function | Ast.AttributedTerm (_, t) -> subst t | Ast.Variable var -> - (try List.assoc var env with Not_found -> assert false) - | (Ast.Literal _ - | Ast.Magic _) as t -> t + let name, expected_ty = CicNotationEnv.declaration_of_var var in + let ty, value = + try + List.assoc name env + with Not_found -> assert false + in + assert (CicNotationEnv.well_typed ty value); (* INVARIANT *) + (* following assertion should be a conditional that makes this + * instantiation fail *) + assert (CicNotationEnv.well_typed expected_ty value); + CicNotationEnv.term_of_value value + | Ast.Magic _ -> assert false (* TO BE IMPLEMENTED *) + | Ast.Literal _ as t -> t | Ast.Layout l -> Ast.Layout (subst_layout l) | t -> CicNotationUtil.visit_ast subst t and subst_layout l = CicNotationUtil.visit_layout subst l in @@ -713,8 +726,18 @@ let load_patterns32 t = set_compiled32 compiled32 let load_patterns21 t = + let rec pp_value = function + | CicNotationEnv.NumValue _ as v -> v + | CicNotationEnv.StringValue _ as v -> v + | CicNotationEnv.TermValue t -> CicNotationEnv.TermValue (pp_ast1 t) + | CicNotationEnv.OptValue None as v -> v + | CicNotationEnv.OptValue (Some v) -> + CicNotationEnv.OptValue (Some (pp_value v)) + | CicNotationEnv.ListValue vl -> + CicNotationEnv.ListValue (List.map pp_value vl) + in let ast_env_of_env env = - List.map (fun (var, term) -> (var, pp_ast1 term)) env + List.map (fun (var, (ty, value)) -> (var, (ty, pp_value value))) env in let fail_k term = pp_ast0 term pp_ast1 in let success_k (env, pid) = instantiate21 (ast_env_of_env env) pid in diff --git a/helm/ocaml/cic_notation/cicNotationTag.ml b/helm/ocaml/cic_notation/cicNotationTag.ml index 67e966823..336f204b7 100644 --- a/helm/ocaml/cic_notation/cicNotationTag.ml +++ b/helm/ocaml/cic_notation/cicNotationTag.ml @@ -49,10 +49,10 @@ let compatible t1 t2 = match t1, t2 with | Variable _, Variable _ -> true | Variable _, _ - | _, Variable _ -> false - | Layout _, _ - | _, Layout _ + | _, Variable _ | Magic _, _ - | _, Magic _ -> assert false + | _, Magic _ -> false + | Layout _, _ + | _, Layout _ -> assert false | _ -> true